1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Johannes Hölzl, Mario Carneiro
  5  -/
  6  
  7  import data.set.countable data.quot logic.function set_theory.schroeder_bernstein
src         └────────────────┘ └───────┘ └────────────┘ └────────────────────────────┘
  8  
  9  /-!
 10  # Cardinal Numbers
 11  
 12  We define cardinal numbers as a quotient of types under the equivalence relation of equinumerity.
 13  We define the order on cardinal numbers, define omega, and do basic cardinal arithmetic:
 14    addition, multiplication, power, cardinal successor, minimum, supremum,
 15      infinitary sums and products
 16  
 17  ## Implementation notes
 18  
 19  * There is a type of cardinal numbers in every universe level: `cardinal.{u} : Type (u + 1)`
 20    is the quotient of types in `Type u`.
 21    There is a lift operation lifting cardinal numbers to a higher level.
 22  * Cardinal arithmetic specifically for infinite cardinals (like `κ * κ = κ`) is in the file
 23    `set_theory/ordinal.lean`, because concepts from that file are used in the proof.
 24  
 25  ## References
 26  
 27  * <https://en.wikipedia.org/wiki/Cardinal_number>
 28  
 29  ## Tags
 30  
 31  cardinal number, cardinal arithmetic, cardinal exponentiation, omega
 32  -/
 33  
 34  open function lattice set
 35  open_locale classical
 36  
 37  universes u v w x
 38  variables {α β : Type u}
 39  
 40  /-- The equivalence relation on types given by equivalence (bijective correspondence) of types.
 41    Quotienting by this equivalence relation gives the cardinal numbers.
 42  -/
 43  instance cardinal.is_equivalent : setoid (Type u) :=
id                                     └────┘
src                                    └────┘
typ                                    └────┘
 44  { r := λα β, nonempty (α ≃ β),
id              └──────┘    
src               └──────┘    
typ             └──────┘    
doc                           
 45    iseqv := ⟨λα,
id                
typ               
 46      ⟨equiv.refl α⟩,
id        └────────┘ 
src       └────────┘
typ       └────────┘ 
 47      λα β ⟨e⟩, ⟨e.symm⟩,
id               └───┘
src                  └───┘
typ              └───┘
 48      λα β γ ⟨e₁⟩ ⟨e₂⟩, ⟨e₁.trans e₂⟩⟩ }
id           └┘  └┘      └────┘
src                           └────┘
typ          └┘  └┘      └────┘
 49  
 50  /-- `cardinal.{u}` is the type of cardinal numbers in `Type u`,
 51    defined as the quotient of `Type u` by existence of an equivalence
 52    (a bijection with explicit inverse). -/
 53  def cardinal : Type (u + 1) := quotient cardinal.is_equivalent
id                                  └──────┘ └────────────────────┘
src                                 └──────┘ └────────────────────┘
typ                                 └──────┘ └────────────────────┘
doc                                          └────────────────────┘
 54  
 55  namespace cardinal
 56  
 57  /-- The cardinal number of a type -/
 58  def mk : Type u → cardinal := quotient.mk
id            └──┘     └──────┘    └─────────┘
src                    └──────┘    └─────────┘
typ           └──┘     └──────┘    └─────────┘
doc                    └──────┘
 59  
 60  localized "notation `#` := cardinal.mk" in cardinal
 61  
 62  protected lemma eq : mk α = mk β ↔ nonempty (α ≃ β) := quotient.eq
id                        └┘   └┘   └──────┘         └─────────┘
src                       └┘    └┘    └──────┘           └─────────┘
typ                       └┘   └┘   └──────┘         └─────────┘
doc                       └┘     └┘                 
 63  
 64  @[simp] theorem mk_def (α : Type u) : @eq cardinal ⟦α⟧ (mk α) := rfl
id                                          └┘ └──────┘   └┘      └─┘
src                                         └┘ └──────┘    └┘       └─┘
typ                                         └┘ └──────┘   └┘      └─┘
doc    └──┘                                    └──────┘      └┘
 65  
 66  @[simp] theorem mk_out (c : cardinal) : mk (c.out) = c := quotient.out_eq _
id                               └──────┘    └┘  └──┘       └─────────────┘
src                              └──────┘    └┘   └──┘        └─────────────┘
typ                              └──────┘    └┘  └──┘       └─────────────┘
doc    └──┘                      └──────┘    └┘   └──┘
 67  
 68  /-- We define the order on cardinal numbers by `mk α ≤ mk β` if and only if
 69    there exists an embedding (injective function) from α to β. -/
 70  instance : has_le cardinal.{u} :=
id              └────┘ └──────┘
src             └────┘ └──────┘
typ             └────┘ └──────┘
doc                    └──────┘
 71  ⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, nonempty $ α ↪ β) $
id     └┘ └┘  └───────────────┘ └┘ └┘      └──────┘     
src           └───────────────┘              └──────┘     
typ    └┘ └┘  └───────────────┘ └┘ └┘      └──────┘     
 72    assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
id                └┘  └┘
typ               └┘  └┘
 73      propext ⟨assume ⟨e⟩, ⟨e.congr e₁ e₂⟩, assume ⟨e⟩, ⟨e.congr e₁.symm e₂.symm⟩⟩⟩
id       └─────┘              └────┘                     └────┘   └───┘   └───┘
src      └─────┘                └────┘                       └────┘   └───┘   └───┘
typ      └─────┘              └────┘                     └────┘   └───┘   └───┘
 74  
 75  theorem mk_le_of_injective {α β : Type u} {f : α → β} (hf : injective f) : mk α ≤ mk β :=
id                                                             └───────┘     └┘   └┘ 
src                                                              └───────┘      └┘    └┘
typ                                                            └───────┘     └┘   └┘ 
doc                                                                             └┘     └┘
 76  ⟨⟨f, hf⟩⟩
id       └┘
typ      └┘
 77  
 78  theorem mk_le_of_surjective {α β : Type u} {f : α → β} (hf : surjective f) : mk β ≤ mk α :=
id                                                              └────────┘     └┘   └┘ 
src                                                               └────────┘      └┘    └┘
typ                                                             └────────┘     └┘   └┘ 
doc                                                                               └┘     └┘
 79  ⟨embedding.of_surjective hf⟩
id    └─────────────────────┘ └┘
src   └─────────────────────┘
typ   └─────────────────────┘ └┘
 80  
 81  theorem le_mk_iff_exists_set {c : cardinal} {α : Type u} :
id                                     └──────┘
src                                    └──────┘
typ                                    └──────┘
doc                                    └──────┘
 82    c ≤ mk α ↔ ∃ p : set α, mk p = c :=
id       └┘        └─┘  └┘   
src       └┘         └─┘   └┘   
typ      └┘        └─┘  └┘   
doc        └┘                  └┘
 83  ⟨quotient.induction_on c $ λ β ⟨⟨f, hf⟩⟩,
id    └───────────────────┘          └┘
src   └───────────────────┘
typ   └───────────────────┘          └┘
 84    ⟨set.range f, eq.symm $ quot.sound ⟨equiv.set.range f hf⟩⟩,
id      └───────┘    └─────┘   └────────┘  └─────────────┘
src     └───────┘    └─────┘   └────────┘  └─────────────┘
typ     └───────┘    └─────┘   └────────┘  └─────────────┘
doc     └───────┘
 85  λ ⟨p, e⟩, e ▸ ⟨⟨subtype.val, λ a b, subtype.eq⟩⟩⟩
id                └─────────┘       └────────┘
src                 └─────────┘         └────────┘
typ               └─────────┘       └────────┘
 86  
 87  theorem out_embedding {c c' : cardinal} : c ≤ c' ↔ nonempty (c.out ↪ c'.out) :=
id                                 └──────┘      └┘  └──────┘  └──┘  └┘└──┘
src                                └──────┘           └──────┘   └──┘    └──┘
typ                                └──────┘      └┘  └──────┘  └──┘  └┘└──┘
doc                                └──────┘                        └──┘     └──┘
 88  by { transitivity _, rw [←quotient.out_eq c, ←quotient.out_eq c'], refl }
id                             └─────────────┘    └─────────────┘ └┘
src       └────────────┘  └───┘└─────────────┘ └─┘└─────────────┘    └───┘
typ       └────────────┘  └───┘└─────────────┘└─┘└─────────────┘└┘  └───┘
doc       └────────────┘  └───┘                └─┘                   └───┘
txt       └────────────┘  └───┘                └─┘                   └───┘
par       └────────────┘  └───┘                └─┘                   └───┘
pid                   └┘    └─┘                └─┘                       
st     └───────────────┘└──────────────────────┘└───────────────────┘└──────┘└┘
 89  
 90  instance : linear_order cardinal.{u} :=
id              └──────────┘ └──────┘
src             └──────────┘ └──────┘
typ             └──────────┘ └──────┘
doc                          └──────┘
 91  { le          := (≤),
id                   
src                  
typ                  
 92    le_refl     := by rintros ⟨α⟩; exact ⟨embedding.refl _⟩,
id                                           └────────────┘
src                      └─────────┘  └────┘ └────────────┘└─┘
typ                      └─────────┘  └────┘ └────────────┘└─┘
doc                      └─────────┘  └────┘               └─┘
txt                      └─────────┘  └────┘               └─┘
par                      └─────────┘  └────┘               └─┘
pid                             └──┘                      └─┘
st                      └────────────────────────────────────┘
 93    le_trans    := by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.trans e₂⟩,
id                                                             └──────┘ └┘
src                      └───────────────────────────┘  └────┘ └──────┘  
typ                      └───────────────────────────┘  └────┘ └──────┘└┘
doc                      └───────────────────────────┘  └────┘           
txt                      └───────────────────────────┘  └────┘           
par                      └───────────────────────────┘  └────┘           
pid                             └────────────────────┘                  
st                      └─────────────────────────────────────────────────┘
 94    le_antisymm := by rintros ⟨α⟩ ⟨β⟩ ⟨e₁⟩ ⟨e₂⟩; exact quotient.sound (e₁.antisymm e₂),
id                                                        └────────────┘  └─────────┘ └┘
src                      └───────────────────────┘  └────┘└────────────┘ └─────────┘  
typ                      └───────────────────────┘  └────┘└────────────┘ └─────────┘└┘
doc                      └───────────────────────┘  └────┘                            
txt                      └───────────────────────┘  └────┘                            
par                      └───────────────────────┘  └────┘                            
pid                             └────────────────┘                                   
st                      └───────────────────────────────────────────────────────────────┘
 95    le_total    := by rintros ⟨α⟩ ⟨β⟩; exact embedding.total }
id                                              └─────────────┘
src                      └─────────────┘  └────┘└─────────────┘
typ                      └─────────────┘  └────┘└─────────────┘
doc                      └─────────────┘  └────┘               
txt                      └─────────────┘  └────┘               
par                      └─────────────┘  └────┘               
pid                             └──────┘                      
st                      └──────────────────────────────────────┘
 96  
 97  noncomputable instance : decidable_linear_order cardinal.{u} := classical.DLO _
id                            └────────────────────┘ └──────┘        └───────────┘
src                           └────────────────────┘ └──────┘        └───────────┘
typ                           └────────────────────┘ └──────┘        └───────────┘
doc                                                  └──────┘
 98  
 99  noncomputable instance : distrib_lattice cardinal.{u} := by apply_instance -- short-circuit type class inference
id                            └─────────────┘ └──────┘
src                           └─────────────┘ └──────┘           └────────────────────────────────────────────────────
typ                           └─────────────┘ └──────┘           └────────────────────────────────────────────────────
doc                           └─────────────┘ └──────┘           └────────────────────────────────────────────────────
txt                                                              └────────────────────────────────────────────────────
par                                                              └────────────────────────────────────────────────────
pid                                                                            └──────────────────────────────────────
st                                                              └─────────────────────────────────────────────────────
100  
src  
typ  
doc  
txt  
par  
pid  
st   
101  instance : has_zero cardinal.{u} := ⟨⟦pempty⟧⟩
id              └──────┘ └──────┘         └────┘
src             └──────┘ └──────┘         └────┘
typ             └──────┘ └──────┘         └────┘
doc                      └──────┘          └────┘
102  
103  instance : inhabited cardinal.{u} := ⟨0⟩
id              └───────┘ └──────┘
src             └───────┘ └──────┘
typ             └───────┘ └──────┘
doc                       └──────┘
104  
105  theorem ne_zero_iff_nonempty {α : Type u} : mk α ≠ 0 ↔ nonempty α :=
id                                               └┘      └──────┘ 
src                                              └┘       └──────┘
typ                                              └┘      └──────┘ 
doc                                              └┘
106  not_iff_comm.1
id   └──────────┘
src  └──────────┘
typ  └──────────┘
107    ⟨λ h, quotient.sound ⟨(equiv.empty_of_not_nonempty h).trans equiv.empty_equiv_pempty⟩,
id          └────────────┘   └─────────────────────────┘  └───┘  └──────────────────────┘
src          └────────────┘   └─────────────────────────┘   └───┘  └──────────────────────┘
typ         └────────────┘   └─────────────────────────┘  └───┘  └──────────────────────┘
108     λ e, let ⟨h⟩ := quotient.exact e in λ ⟨a⟩, (h a).elim⟩
id          └─┘       └────────────┘               └──┘
src                     └────────────┘                  └──┘
typ         └─┘       └────────────┘               └──┘
109  
110  instance : has_one cardinal.{u} := ⟨⟦punit⟧⟩
id              └─────┘ └──────┘         └───┘
src             └─────┘ └──────┘         └───┘
typ             └─────┘ └──────┘         └───┘
doc                     └──────┘
111  
112  instance : zero_ne_one_class cardinal.{u} :=
id              └───────────────┘ └──────┘
src             └───────────────┘ └──────┘
typ             └───────────────┘ └──────┘
doc                               └──────┘
113  { zero := 0, one := 1, zero_ne_one :=
114    ne.symm $ ne_zero_iff_nonempty.2 ⟨punit.star⟩ }
id     └─────┘   └──────────────────┘   └────────┘
src    └─────┘   └──────────────────┘   └────────┘
typ    └─────┘   └──────────────────┘   └────────┘
115  
116  theorem le_one_iff_subsingleton {α : Type u} : mk α ≤ 1 ↔ subsingleton α :=
id                                                  └┘      └──────────┘ 
src                                                 └┘       └──────────┘
typ                                                 └┘      └──────────┘ 
doc                                                 └┘
117  ⟨λ ⟨f⟩, ⟨λ a b, f.inj (subsingleton.elim _ _)⟩,
id                └──┘  └───────────────┘
src                   └──┘  └───────────────┘
typ               └──┘  └───────────────┘
118   λ ⟨h⟩, ⟨⟨λ a, punit.star, λ a b _, h _ _⟩⟩⟩
id               └────────┘      
src                 └────────┘
typ              └────────┘      
119  
120  instance : has_add cardinal.{u} :=
id              └─────┘ └──────┘
src             └─────┘ └──────┘
typ             └─────┘ └──────┘
doc                     └──────┘
121  ⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, mk (α ⊕ β)) $ assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
id     └┘ └┘  └───────────────┘ └┘ └┘      └┘                    └┘  └┘
src           └───────────────┘              └┘    
typ    └┘ └┘  └───────────────┘ └┘ └┘      └┘                    └┘  └┘
doc                                          └┘
122    quotient.sound ⟨equiv.sum_congr e₁ e₂⟩⟩
id     └────────────┘  └─────────────┘
src    └────────────┘  └─────────────┘
typ    └────────────┘  └─────────────┘
123  
124  @[simp] theorem add_def (α β) : mk α + mk β = mk (α ⊕ β) := rfl
id                                   └┘   └┘   └┘         └─┘
src                                  └┘    └┘    └┘           └─┘
typ                                  └┘   └┘   └┘         └─┘
doc    └──┘                          └┘     └┘     └┘
125  
126  instance : has_mul cardinal.{u} :=
id              └─────┘ └──────┘
src             └─────┘ └──────┘
typ             └─────┘ └──────┘
doc                     └──────┘
127  ⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, mk (α × β)) $ assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
id     └┘ └┘  └───────────────┘ └┘ └┘      └┘                    └┘  └┘
src           └───────────────┘              └┘    
typ    └┘ └┘  └───────────────┘ └┘ └┘      └┘                    └┘  └┘
doc                                          └┘
128    quotient.sound ⟨equiv.prod_congr e₁ e₂⟩⟩
id     └────────────┘  └──────────────┘
src    └────────────┘  └──────────────┘
typ    └────────────┘  └──────────────┘
129  
130  @[simp] theorem mul_def (α β : Type u) : mk α * mk β = mk (α × β) := rfl
id                                            └┘   └┘   └┘         └─┘
src                                           └┘    └┘    └┘           └─┘
typ                                           └┘   └┘   └┘         └─┘
doc    └──┘                                   └┘     └┘     └┘
131  
132  private theorem add_comm (a b : cardinal.{u}) : a + b = b + a :=
id                                   └──────┘              
src                                  └──────┘                
typ                                  └──────┘              
doc                                  └──────┘
133  quotient.induction_on₂ a b $ assume α β, quotient.sound ⟨equiv.sum_comm α β⟩
id   └────────────────────┘               └────────────┘  └────────────┘  
src  └────────────────────┘                   └────────────┘  └────────────┘
typ  └────────────────────┘               └────────────┘  └────────────┘  
134  
135  private theorem mul_comm (a b : cardinal.{u}) : a * b = b * a :=
id                                   └──────┘              
src                                  └──────┘                
typ                                  └──────┘              
doc                                  └──────┘
136  quotient.induction_on₂ a b $ assume α β, quotient.sound ⟨equiv.prod_comm α β⟩
id   └────────────────────┘               └────────────┘  └─────────────┘  
src  └────────────────────┘                   └────────────┘  └─────────────┘
typ  └────────────────────┘               └────────────┘  └─────────────┘  
137  
138  private theorem zero_add (a : cardinal.{u}) : 0 + a = a :=
id                                 └──────┘             
src                                └──────┘             
typ                                └──────┘             
doc                                └──────┘
139  quotient.induction_on a $ assume α, quotient.sound ⟨equiv.pempty_sum α⟩
id   └───────────────────┘             └────────────┘  └──────────────┘ 
src  └───────────────────┘               └────────────┘  └──────────────┘
typ  └───────────────────┘             └────────────┘  └──────────────┘ 
140  
141  private theorem zero_mul (a : cardinal.{u}) : 0 * a = 0 :=
id                                 └──────┘            
src                                └──────┘             
typ                                └──────┘            
doc                                └──────┘
142  quotient.induction_on a $ assume α, quotient.sound ⟨equiv.pempty_prod α⟩
id   └───────────────────┘             └────────────┘  └───────────────┘ 
src  └───────────────────┘               └────────────┘  └───────────────┘
typ  └───────────────────┘             └────────────┘  └───────────────┘ 
143  
144  private theorem one_mul (a : cardinal.{u}) : 1 * a = a :=
id                                └──────┘             
src                               └──────┘             
typ                               └──────┘             
doc                               └──────┘
145  quotient.induction_on a $ assume α, quotient.sound ⟨equiv.punit_prod α⟩
id   └───────────────────┘             └────────────┘  └──────────────┘ 
src  └───────────────────┘               └────────────┘  └──────────────┘
typ  └───────────────────┘             └────────────┘  └──────────────┘ 
146  
147  private theorem left_distrib (a b c : cardinal.{u}) : a * (b + c) = a * b + a * c :=
id                                         └──────┘                      
src                                        └──────┘                           
typ                                        └──────┘                      
doc                                        └──────┘
148  quotient.induction_on₃ a b c $ assume α β γ, quotient.sound ⟨equiv.prod_sum_distrib α β γ⟩
id   └────────────────────┘                 └────────────┘  └────────────────────┘   
src  └────────────────────┘                       └────────────┘  └────────────────────┘
typ  └────────────────────┘                 └────────────┘  └────────────────────┘   
149  
150  instance : comm_semiring cardinal.{u} :=
id              └───────────┘ └──────┘
src             └───────────┘ └──────┘
typ             └───────────┘ └──────┘
doc                           └──────┘
151  { zero          := 0,
152    one           := 1,
153    add           := (+),
id                      
src                     
typ                     
154    mul           := (*),
id                      
src                     
typ                     
155    zero_add      := zero_add,
id                      └──────┘
src                     └──────┘
typ                     └──────┘
156    add_zero      := assume a, by rw [add_comm a 0, zero_add a],
id                                      └──────┘     └──────┘ 
src                                  └──┘└──────┘ └──┘└──────┘ 
typ                                 └──┘└──────┘└──┘└──────┘
doc                                  └──┘         └──┘         
txt                                  └──┘         └──┘         
par                                  └──┘         └──┘         
pid                                    └┘         └──┘         
st                                  └──────────────┘└───────────┘
157    add_assoc     := λa b c, quotient.induction_on₃ a b c $ assume α β γ,
id                           └────────────────────┘               
src                             └────────────────────┘
typ                          └────────────────────┘               
158      quotient.sound ⟨equiv.sum_assoc α β γ⟩,
id       └────────────┘  └─────────────┘   
src      └────────────┘  └─────────────┘
typ      └────────────┘  └─────────────┘   
159    add_comm      := add_comm,
id                      └──────┘
src                     └──────┘
typ                     └──────┘
160    zero_mul      := zero_mul,
id                      └──────┘
src                     └──────┘
typ                     └──────┘
161    mul_zero      := assume a, by rw [mul_comm a 0, zero_mul a],
id                                      └──────┘     └──────┘ 
src                                  └──┘└──────┘ └──┘└──────┘ 
typ                                 └──┘└──────┘└──┘└──────┘
doc                                  └──┘         └──┘         
txt                                  └──┘         └──┘         
par                                  └──┘         └──┘         
pid                                    └┘         └──┘         
st                                  └──────────────┘└───────────┘
162    one_mul       := one_mul,
id                      └─────┘
src                     └─────┘
typ                     └─────┘
163    mul_one       := assume a, by rw [mul_comm a 1, one_mul a],
id                                      └──────┘     └─────┘ 
src                                  └──┘└──────┘ └──┘└─────┘ 
typ                                 └──┘└──────┘└──┘└─────┘
doc                                  └──┘         └──┘        
txt                                  └──┘         └──┘        
par                                  └──┘         └──┘        
pid                                    └┘         └──┘        
st                                  └──────────────┘└──────────┘
164    mul_assoc     := λa b c, quotient.induction_on₃ a b c $ assume α β γ,
id                           └────────────────────┘               
src                             └────────────────────┘
typ                          └────────────────────┘               
165      quotient.sound ⟨equiv.prod_assoc α β γ⟩,
id       └────────────┘  └──────────────┘   
src      └────────────┘  └──────────────┘
typ      └────────────┘  └──────────────┘   
166    mul_comm      := mul_comm,
id                      └──────┘
src                     └──────┘
typ                     └──────┘
167    left_distrib  := left_distrib,
id                      └──────────┘
src                     └──────────┘
typ                     └──────────┘
168    right_distrib := assume a b c,
id                               
typ                              
169      by rw [mul_comm (a + b) c, left_distrib c a b, mul_comm c a, mul_comm c b] }
id              └──────┘        └──────────┘     └──────┘    └──────┘  
src         └──┘└──────┘   └┘ └┘└──────────┘   └┘└──────┘  └┘└──────┘  └┘
typ         └──┘└──────┘ └┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘
doc         └──┘            └┘ └┘               └┘          └┘          └┘
txt         └──┘            └┘ └┘               └┘          └┘          └┘
par         └──┘            └┘ └┘               └┘          └┘          └┘
pid           └┘            └┘ └┘               └┘          └┘          
st         └─────────────────────┘└──────────────────┘└────────────┘└────────────┘
170  
171  /-- The cardinal exponential. `mk α ^ mk β` is the cardinal of `β → α`. -/
172  protected def power (a b : cardinal.{u}) : cardinal.{u} :=
id                              └──────┘        └──────┘
src                             └──────┘        └──────┘
typ                             └──────┘        └──────┘
doc                             └──────┘        └──────┘
173  quotient.lift_on₂ a b (λα β, mk (β → α)) $ assume α₁ α₂ β₁ β₂ ⟨e₁⟩ ⟨e₂⟩,
id   └───────────────┘        └┘                 └┘ └┘ └┘ └┘ └┘  └┘
src  └───────────────┘            └┘
typ  └───────────────┘        └┘                 └┘ └┘ └┘ └┘ └┘  └┘
doc                               └┘
174    quotient.sound ⟨equiv.arrow_congr e₂ e₁⟩
id     └────────────┘  └───────────────┘
src    └────────────┘  └───────────────┘
typ    └────────────┘  └───────────────┘
175  
176  instance : has_pow cardinal cardinal := ⟨cardinal.power⟩
id              └─────┘ └──────┘ └──────┘     └────────────┘
src             └─────┘ └──────┘ └──────┘     └────────────┘
typ             └─────┘ └──────┘ └──────┘     └────────────┘
doc                     └──────┘ └──────┘     └────────────┘
177  local infixr ^ := @has_pow.pow cardinal cardinal cardinal.has_pow
id                      └─────────┘ └──────┘ └──────┘ └──────────────┘
src                     └─────────┘ └──────┘ └──────┘ └──────────────┘
typ                     └─────────┘ └──────┘ └──────┘ └──────────────┘
doc                                 └──────┘ └──────┘
178  
179  @[simp] theorem power_def (α β) : mk α ^ mk β = mk (β → α) := rfl
id                                     └┘   └┘   └┘          └─┘
src                                    └┘    └┘    └┘            └─┘
typ                                    └┘   └┘   └┘          └─┘
doc    └──┘                            └┘    └┘     └┘
180  
181  @[simp] theorem power_zero {a : cardinal} : a ^ 0 = 1 :=
id                                   └──────┘        
src                                  └──────┘         
typ                                  └──────┘        
doc    └──┘                          └──────┘      
182  quotient.induction_on a $ assume α, quotient.sound
id   └───────────────────┘             └────────────┘
src  └───────────────────┘               └────────────┘
typ  └───────────────────┘             └────────────┘
183  ⟨equiv.pempty_arrow_equiv_punit α⟩
id    └────────────────────────────┘ 
src   └────────────────────────────┘
typ   └────────────────────────────┘ 
184  
185  @[simp] theorem power_one {a : cardinal} : a ^ 1 = a :=
id                                  └──────┘         
src                                 └──────┘         
typ                                 └──────┘         
doc    └──┘                         └──────┘      
186  quotient.induction_on a $ assume α, quotient.sound
id   └───────────────────┘             └────────────┘
src  └───────────────────┘               └────────────┘
typ  └───────────────────┘             └────────────┘
187  ⟨equiv.punit_arrow_equiv α⟩
id    └─────────────────────┘ 
src   └─────────────────────┘
typ   └─────────────────────┘ 
188  
189  @[simp] theorem one_power {a : cardinal} : 1 ^ a = 1 :=
id                                  └──────┘        
src                                 └──────┘         
typ                                 └──────┘        
doc    └──┘                         └──────┘      
190  quotient.induction_on a $ assume α, quotient.sound
id   └───────────────────┘             └────────────┘
src  └───────────────────┘               └────────────┘
typ  └───────────────────┘             └────────────┘
191  ⟨equiv.arrow_punit_equiv_punit α⟩
id    └───────────────────────────┘ 
src   └───────────────────────────┘
typ   └───────────────────────────┘ 
192  
193  @[simp] theorem prop_eq_two : mk (ulift Prop) = 2 :=
id                                 └┘  └───┘       
src                                └┘  └───┘       
typ                                └┘  └───┘       
doc    └──┘                        └┘  └───┘
194  quot.sound ⟨equiv.ulift.trans $ equiv.Prop_equiv_bool.trans equiv.bool_equiv_punit_sum_punit⟩
id   └────────┘  └─────────┘└────┘   └───────────────────┘└────┘ └──────────────────────────────┘
src  └────────┘  └─────────┘└────┘   └───────────────────┘└────┘ └──────────────────────────────┘
typ  └────────┘  └─────────┘└────┘   └───────────────────┘└────┘ └──────────────────────────────┘
195  
196  @[simp] theorem zero_power {a : cardinal} : a ≠ 0 → 0 ^ a = 0 :=
id                                   └──────┘              
src                                  └──────┘                
typ                                  └──────┘              
doc    └──┘                          └──────┘              
197  quotient.induction_on a $ assume α heq,
id   └───────────────────┘            └─┘
src  └───────────────────┘              └─┘
typ  └───────────────────┘            └─┘
198  nonempty.rec_on (ne_zero_iff_nonempty.1 heq) $ assume a,
id   └─────────────┘  └──────────────────┘  └─┘           
src  └─────────────┘  └──────────────────┘  └─┘
typ  └─────────────┘  └──────────────────┘  └─┘           
199  quotient.sound ⟨equiv.equiv_pempty $ assume f, pempty.rec (λ _, false) (f a)⟩
id   └────────────┘  └────────────────┘            └────────┘      └───┘    
src  └────────────┘  └────────────────┘             └────────┘       └───┘
typ  └────────────┘  └────────────────┘            └────────┘      └───┘    
200  
201  theorem power_ne_zero {a : cardinal} (b) : a ≠ 0 → a ^ b ≠ 0 :=
id                              └──────┘                 
src                             └──────┘                    
typ                             └──────┘                 
doc                             └──────┘                  
202  quotient.induction_on₂ a b $ λ α β h,
id   └────────────────────┘         
src  └────────────────────┘
typ  └────────────────────┘         
203  let ⟨a⟩ := ne_zero_iff_nonempty.1 h in
id   └─┘       └──────────────────┘  
src             └──────────────────┘
typ  └─┘       └──────────────────┘  
204  ne_zero_iff_nonempty.2 ⟨λ _, a⟩
id   └──────────────────┘     
src  └──────────────────┘
typ  └──────────────────┘     
205  
206  theorem mul_power {a b c : cardinal} : (a * b) ^ c = a ^ c * b ^ c :=
id                              └──────┘                  
src                             └──────┘                       
typ                             └──────┘                  
doc                             └──────┘                          
207  quotient.induction_on₃ a b c $ assume α β γ,
id   └────────────────────┘               
src  └────────────────────┘
typ  └────────────────────┘               
208    quotient.sound ⟨equiv.arrow_prod_equiv_prod_arrow α β γ⟩
id     └────────────┘  └───────────────────────────────┘   
src    └────────────┘  └───────────────────────────────┘
typ    └────────────┘  └───────────────────────────────┘   
209  
210  theorem power_add {a b c : cardinal} : a ^ (b + c) = a ^ b * a ^ c :=
id                              └──────┘                  
src                             └──────┘                       
typ                             └──────┘                  
doc                             └──────┘                          
211  quotient.induction_on₃ a b c $ assume α β γ,
id   └────────────────────┘               
src  └────────────────────┘
typ  └────────────────────┘               
212    quotient.sound ⟨equiv.sum_arrow_equiv_prod_arrow β γ α⟩
id     └────────────┘  └──────────────────────────────┘   
src    └────────────┘  └──────────────────────────────┘
typ    └────────────┘  └──────────────────────────────┘   
213  
214  theorem power_mul {a b c : cardinal} : (a ^ b) ^ c = a ^ (b * c) :=
id                              └──────┘                 
src                             └──────┘                     
typ                             └──────┘                 
doc                             └──────┘                  
215  by rw [_root_.mul_comm b c];
id          └─────────────┘  
src     └──┘└─────────────┘  
typ     └──┘└─────────────┘
doc     └──┘                 
txt     └──┘                 
par     └──┘                 
pid       └┘                 
st     └──────────────────────┘└─
216  from (quotient.induction_on₃ a b c $ assume α β γ,
id         └────────────────────┘   
src  └───┘ └────────────────────┘          └───────
typ  └───┘ └────────────────────┘       └───────
doc  └───┘                                 └───────
txt  └───┘                                 └───────
par  └───┘                                 └───────
pid  └───┘                                 └───────
st   ───────────────────────────────────────────────────
217    quotient.sound ⟨equiv.arrow_arrow_equiv_prod_arrow γ β α⟩)
id     └────────────┘  └────────────────────────────────┘
src  ─┘└────────────┘ └────────────────────────────────┘   └──
typ  ─┘└────────────┘ └────────────────────────────────┘   └──
doc  ─┘                                                    └──
txt  ─┘                                                    └──
par  ─┘                                                    └──
pid  ─┘                                                    └┘
st   ─────────────────────────────────────────────────────────────
218  
src  
typ  
doc  
txt  
par  
pid  
st   
219  @[simp] lemma pow_cast_right (κ : cardinal.{u}) :
id                                     └──────┘
src                                    └──────┘
typ                                    └──────┘
doc    └──┘                            └──────┘
220    ∀ n : ℕ, (κ ^ (↑n : cardinal.{u})) = @has_pow.pow _ _ monoid.has_pow κ n
id                   └──────┘         └─────────┘     └────────────┘  
src                     └──────┘         └─────────┘     └────────────┘
typ                  └──────┘         └─────────┘     └────────────┘  
doc                       └──────┘
221  | 0 := by simp
src            └───┘
typ            └───┘
doc            └───┘
txt            └───┘
par            └───┘
pid                
st            └────┘
222  | (_+1) := by rw [nat.cast_succ, power_add, power_one, _root_.mul_comm, pow_succ, pow_cast_right]
id                    └───────────┘  └───────┘  └───────┘  └─────────────┘  └──────┘  └────────────┘
src               └──┘└───────────┘└┘└───────┘└┘└───────┘└┘└─────────────┘└┘└──────┘└┘              └─
typ               └──┘└───────────┘└┘└───────┘└┘└───────┘└┘└─────────────┘└┘└──────┘└┘└────────────┘└─
doc                └──┘             └┘         └┘         └┘               └┘        └┘              └─
txt                └──┘             └┘         └┘         └┘               └┘        └┘              └─
par                └──┘             └┘         └┘         └┘               └┘        └┘              └─
pid                  └┘             └┘         └┘         └┘               └┘        └┘              
st                └────────────────┘└─────────┘└─────────┘└───────────────┘└────────┘└──────────────┘
223  
src  
typ  
doc  
txt  
par  
pid  
st   
224  section order_properties
225  open sum
226  
227  theorem zero_le : ∀(a : cardinal), 0 ≤ a :=
id                           └──────┘      
src                          └──────┘     
typ                          └──────┘      
doc                          └──────┘
228  by rintro ⟨α⟩; exact ⟨embedding.of_not_nonempty $ λ ⟨a⟩, a.elim⟩
id                         └───────────────────────┘          └───┘
src     └────────┘  └────┘ └───────────────────────┘  └┘ └─┘ └───┘└─
typ     └────────┘  └────┘ └───────────────────────┘  └┘└─┘ └───┘└─
doc     └────────┘  └────┘                            └┘ └─┘      └─
txt     └────────┘  └────┘                            └┘ └─┘      └─
par     └────────┘  └────┘                            └┘ └─┘      └─
pid           └──┘                                   └┘ └─┘      
st     └──────────────────────────────────────────────────────────────
229  
src  
typ  
doc  
txt  
par  
pid  
st   
230  theorem le_zero (a : cardinal) : a ≤ 0 ↔ a = 0 :=
id                        └──────┘          
src                       └──────┘            
typ                       └──────┘          
doc                       └──────┘
231  by simp [le_antisymm_iff, zero_le]
id            └─────────────┘  └─────┘
src     └────┘└─────────────┘└┘└─────┘└─
typ     └────┘└─────────────┘└┘└─────┘└─
doc     └────┘               └┘       └─
txt     └────┘               └┘       └─
par     └────┘               └┘       └─
pid                        └┘       
st     └────────────────────────────────
232  
src  
typ  
doc  
txt  
par  
pid  
st   
233  theorem pos_iff_ne_zero {o : cardinal} : 0 < o ↔ o ≠ 0 :=
id                                └──────┘          
src                               └──────┘            
typ                               └──────┘          
doc                               └──────┘
234  by simp [lt_iff_le_and_ne, eq_comm, zero_le]
id            └──────────────┘  └─────┘  └─────┘
src     └────┘└──────────────┘└┘└─────┘└┘└─────┘└─
typ     └────┘└──────────────┘└┘└─────┘└┘└─────┘└─
doc     └────┘                └┘       └┘       └─
txt     └────┘                └┘       └┘       └─
par     └────┘                └┘       └┘       └─
pid                         └┘       └┘       
st     └──────────────────────────────────────────
235  
src  
typ  
doc  
txt  
par  
pid  
st   
236  theorem zero_lt_one : (0 : cardinal) < 1 :=
id                              └──────┘  
src                             └──────┘  
typ                             └──────┘  
doc                             └──────┘
237  lt_of_le_of_ne (zero_le _) zero_ne_one
id   └────────────┘  └─────┘    └─────────┘
src  └────────────┘  └─────┘    └─────────┘
typ  └────────────┘  └─────┘    └─────────┘
238  
239  lemma zero_power_le (c : cardinal.{u}) : (0 : cardinal.{u}) ^ c ≤ 1 :=
id                            └──────┘             └──────┘        
src                           └──────┘             └──────┘         
typ                           └──────┘             └──────┘        
doc                           └──────┘             └──────┘      
240  by { by_cases h : c = 0, rw [h, power_zero], rw [zero_power h], apply zero_le }
id                                └────────┘       └────────┘          └─────┘
src       └───────┘ └─┘ └┘  └──┘ └┘└────────┘  └──┘└────────┘   └────┘└─────┘
typ       └───────┘ └─┘└┘  └──┘└┘└────────┘  └──┘└────────┘  └────┘└─────┘
doc       └───────┘ └─┘  └┘  └──┘ └┘            └──┘             └────┘       
txt       └───────┘ └─┘  └┘  └──┘ └┘            └──┘             └────┘       
par       └───────┘ └─┘  └┘  └──┘ └┘            └──┘             └────┘       
pid                └─┘      └┘ └┘              └┘                         
st     └───────────────────┘└─────┘└──────────┘└─────────────────┘└───────────────┘└┘
241  
242  theorem add_le_add : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d :=
id                                    └──────┘                   
src                                   └──────┘                         
typ                                   └──────┘                   
doc                                   └──────┘
243  by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨embedding.sum_congr e₁ e₂⟩
id                                                └─────────────────┘ └┘ └┘
src     └───────────────────────────────┘  └────┘ └─────────────────┘    └─
typ     └───────────────────────────────┘  └────┘ └─────────────────┘└┘└┘└─
doc     └───────────────────────────────┘  └────┘                        └─
txt     └───────────────────────────────┘  └────┘                        └─
par     └───────────────────────────────┘  └────┘                        └─
pid            └────────────────────────┘                               
st     └─────────────────────────────────────────────────────────────────────
244  
src  
typ  
doc  
txt  
par  
pid  
st   
245  theorem add_le_add_left (a) {b c : cardinal} : b ≤ c → a + b ≤ a + c :=
id                                      └──────┘               
src                                     └──────┘                   
typ                                     └──────┘               
doc                                     └──────┘
246  add_le_add (le_refl _)
id   └────────┘  └─────┘
src  └────────┘  └─────┘
typ  └────────┘  └─────┘
247  
248  theorem add_le_add_right {a b : cardinal} (c) (h : a ≤ b) : a + c ≤ b + c :=
id                                   └──────┘                       
src                                  └──────┘                           
typ                                  └──────┘                       
doc                                  └──────┘
249  add_le_add h (le_refl _)
id   └────────┘   └─────┘
src  └────────┘    └─────┘
typ  └────────┘   └─────┘
250  
251  theorem le_add_right (a b : cardinal) : a ≤ a + b :=
id                               └──────┘        
src                              └──────┘         
typ                              └──────┘        
doc                              └──────┘
252  by simpa using add_le_add_left a (zero_le b)
id                  └─────────────┘   └─────┘ 
src     └──────────┘└─────────────┘  └─────┘ └─
typ     └──────────┘└─────────────┘ └─────┘└─
doc     └──────────┘                         └─
txt     └──────────┘                         └─
par     └──────────┘                         └─
pid          └────┘                         
st     └──────────────────────────────────────────
253  
src  
typ  
doc  
txt  
par  
pid  
st   
254  theorem le_add_left (a b : cardinal) : a ≤ b + a :=
id                              └──────┘        
src                             └──────┘         
typ                             └──────┘        
doc                             └──────┘
255  by simpa using add_le_add_right a (zero_le b)
id                  └──────────────┘   └─────┘ 
src     └──────────┘└──────────────┘  └─────┘ └─
typ     └──────────┘└──────────────┘ └─────┘└─
doc     └──────────┘                          └─
txt     └──────────┘                          └─
par     └──────────┘                          └─
pid          └────┘                          
st     └───────────────────────────────────────────
256  
src  
typ  
doc  
txt  
par  
pid  
st   
257  theorem mul_le_mul : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a * c ≤ b * d :=
id                                    └──────┘                   
src                                   └──────┘                         
typ                                   └──────┘                   
doc                                   └──────┘
258  by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨embedding.prod_congr e₁ e₂⟩
id                                                └──────────────────┘ └┘ └┘
src     └───────────────────────────────┘  └────┘ └──────────────────┘    └─
typ     └───────────────────────────────┘  └────┘ └──────────────────┘└┘└┘└─
doc     └───────────────────────────────┘  └────┘                         └─
txt     └───────────────────────────────┘  └────┘                         └─
par     └───────────────────────────────┘  └────┘                         └─
pid            └────────────────────────┘                                
st     └──────────────────────────────────────────────────────────────────────
259  
src  
typ  
doc  
txt  
par  
pid  
st   
260  theorem mul_le_mul_left (a) {b c : cardinal} : b ≤ c → a * b ≤ a * c :=
id                                      └──────┘               
src                                     └──────┘                   
typ                                     └──────┘               
doc                                     └──────┘
261  mul_le_mul (le_refl _)
id   └────────┘  └─────┘
src  └────────┘  └─────┘
typ  └────────┘  └─────┘
262  
263  theorem mul_le_mul_right {a b : cardinal} (c) (h : a ≤ b) : a * c ≤ b * c :=
id                                   └──────┘                       
src                                  └──────┘                           
typ                                  └──────┘                       
doc                                  └──────┘
264  mul_le_mul h (le_refl _)
id   └────────┘   └─────┘
src  └────────┘    └─────┘
typ  └────────┘   └─────┘
265  
266  theorem power_le_power_left : ∀{a b c : cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=
id                                           └──────┘                    
src                                          └──────┘                         
typ                                          └──────┘                    
doc                                          └──────┘                            
267  by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩; exact
src     └────────────────────────┘  └─────
typ     └────────────────────────┘  └─────
doc     └────────────────────────┘  └─────
txt     └────────────────────────┘  └─────
par     └────────────────────────┘  └─────
pid            └─────────────────┘       
st     └──────────────────────────────────
268    let ⟨a⟩ := ne_zero_iff_nonempty.1 hα in
id               └──────────────────┘   └┘
src  ─┘     └───┘└──────────────────┘└─┘  └───
typ  ─┘    └───┘└──────────────────┘└─┘└┘└───
doc  ─┘     └───┘                    └─┘  └───
txt  ─┘     └───┘                    └─┘  └───
par  ─┘     └───┘                    └─┘  └───
pid  ─┘     └───┘                    └─┘  └───
st   ──────────────────────────────────────────
269    ⟨@embedding.arrow_congr_right _ _ _ ⟨a⟩ e⟩
id       └─────────────────────────┘           
src  ─┘  └─────────────────────────┘└─────┘  └┘ └─
typ  ─┘  └─────────────────────────┘└─────┘  └┘└─
doc  ─┘                             └─────┘  └┘ └─
txt  ─┘                             └─────┘  └┘ └─
par  ─┘                             └─────┘  └┘ └─
pid  ─┘                             └─────┘  └┘ 
st   ─────────────────────────────────────────────
270  
src  
typ  
doc  
txt  
par  
pid  
st   
271  theorem power_le_max_power_one {a b c : cardinal} (h : b ≤ c) : a ^ b ≤ max (a ^ c) 1 :=
id                                           └──────┘                 └─┘    
src                                          └──────┘                     └─┘    
typ                                          └──────┘                 └─┘    
doc                                          └──────┘                              
272  begin
st   └─────
273    by_cases ha : a = 0,
id                    
src    └───────┘  └─┘ └┘
typ    └───────┘  └─┘└┘
doc    └───────┘  └─┘  └┘
txt    └───────┘  └─┘  └┘
par    └───────┘  └─┘  └┘
pid              └─┘  
st   ────────────────────┘└─
274    simp [ha, zero_power_le],
id           └┘  └───────────┘
src    └────┘  └┘└───────────┘
typ    └────┘└┘└┘└───────────┘
doc    └────┘  └┘             
txt    └────┘  └┘             
par    └────┘  └┘             
pid          └┘             
st   ─────────────────────────┘└─
275    exact le_trans (power_le_power_left ha h) (le_max_left _ _)
id           └──────┘  └─────────────────┘ └┘    └─────────┘
src    └────┘└──────┘ └─────────────────┘   └┘ └─────────┘└────┘
typ    └────┘└──────┘ └─────────────────┘└┘└┘ └─────────┘└────┘
doc    └────┘                               └┘            └────┘
txt    └────┘                               └┘            └────┘
par    └────┘                               └┘            └────┘
pid                                        └┘            └───┘
st   ─────────────────────────────────────────────────────────────┘
276  end
st   └─┘
277  
278  theorem power_le_power_right {a b c : cardinal} : a ≤ b → a ^ c ≤ b ^ c :=
id                                         └──────┘               
src                                        └──────┘                   
typ                                        └──────┘               
doc                                        └──────┘                     
279  quotient.induction_on₃ a b c $ assume α β γ ⟨e⟩, ⟨embedding.arrow_congr_left e⟩
id   └────────────────────┘                    └────────────────────────┘
src  └────────────────────┘                            └────────────────────────┘
typ  └────────────────────┘                    └────────────────────────┘
280  
281  theorem le_iff_exists_add {a b : cardinal} : a ≤ b ↔ ∃ c, b = a + c :=
id                                    └──────┘              
src                                   └──────┘                  
typ                                   └──────┘              
doc                                   └──────┘
282  ⟨quotient.induction_on₂ a b $ λ α β ⟨⟨f, hf⟩⟩,
id    └────────────────────┘            └┘
src   └────────────────────┘
typ   └────────────────────┘            └┘
283    have (α ⊕ ↥-range f) ≃ β, from
id             └───┘     
src             └───┘    
typ            └───┘     
doc                └───┘    
284      (equiv.sum_congr (equiv.set.range f hf) (equiv.refl _)).trans $
id        └─────────────┘  └─────────────┘        └────────┘    └───┘
src       └─────────────┘  └─────────────┘        └────────┘    └───┘
typ       └─────────────┘  └─────────────┘        └────────┘    └───┘
285      (equiv.set.sum_compl (range f)),
id        └─────────────────┘  └───┘
src       └─────────────────┘  └───┘
typ       └─────────────────┘  └───┘
doc                            └───┘
286    ⟨⟦(-range f : set β)⟧, quotient.sound ⟨this.symm⟩⟩,
id       └───┘     └─┘    └────────────┘  └──┘└───┘
src      └───┘     └─┘     └────────────┘      └───┘
typ      └───┘     └─┘    └────────────┘  └──┘└───┘
doc        └───┘
287   λ ⟨c, e⟩, add_zero a ▸ e.symm ▸ add_le_add_left _ (zero_le _)⟩
id            └──────┘    └───┘  └─────────────┘    └─────┘
src             └──────┘     └───┘  └─────────────┘    └─────┘
typ           └──────┘    └───┘  └─────────────┘    └─────┘
288  
289  end order_properties
290  
291  instance : order_bot cardinal.{u} :=
id              └───────┘ └──────┘
src             └───────┘ └──────┘
typ             └───────┘ └──────┘
doc             └───────┘ └──────┘
292  { bot := 0, bot_le := zero_le, ..cardinal.linear_order }
id                         └─────┘    └───────────────────┘
src                        └─────┘    └───────────────────┘
typ                        └─────┘    └───────────────────┘
293  
294  instance : canonically_ordered_monoid cardinal.{u} :=
id              └────────────────────────┘ └──────┘
src             └────────────────────────┘ └──────┘
typ             └────────────────────────┘ └──────┘
doc             └────────────────────────┘ └──────┘
295  { add_le_add_left       := λ a b h c, add_le_add_left _ h,
id                                     └─────────────┘   
src                                        └─────────────┘
typ                                    └─────────────┘   
296    lt_of_add_lt_add_left := λ a b c, lt_imp_lt_of_le_imp_le (add_le_add_left _),
id                                    └────────────────────┘  └─────────────┘
src                                      └────────────────────┘  └─────────────┘
typ                                   └────────────────────┘  └─────────────┘
297    le_iff_exists_add     := @le_iff_exists_add,
id                               └───────────────┘
src                              └───────────────┘
typ                              └───────────────┘
298    ..cardinal.lattice.order_bot,
id       └────────────────────────┘
src      └────────────────────────┘
typ      └────────────────────────┘
299    ..cardinal.comm_semiring, ..cardinal.linear_order }
id       └────────────────────┘    └───────────────────┘
src      └────────────────────┘    └───────────────────┘
typ      └────────────────────┘    └───────────────────┘
300  
301  theorem cantor : ∀(a : cardinal.{u}), a < 2 ^ a :=
id                          └──────┘            
src                         └──────┘            
typ                         └──────┘            
doc                         └──────┘             
302  by rw ← prop_eq_two; rintros ⟨a⟩; exact ⟨
id           └─────────┘
src     └───┘└─────────┘  └─────────┘  └────┘ 
typ     └───┘└─────────┘  └─────────┘  └────┘ 
doc     └───┘             └─────────┘  └────┘ 
txt     └───┘             └─────────┘  └────┘ 
par     └───┘             └─────────┘  └────┘ 
pid       └─┘                    └──┘        
st     └───────────────────────────────────────
303    ⟨⟨λ a b, ⟨a = b⟩, λ a b h, cast (ulift.up.inj (@congr_fun _ _ _ _ h b)).symm rfl⟩⟩,
id                               └──┘  └──────────┘   └───────┘                    └─┘
src  ─┘   └────┘   └─┘ └──────┘└──┘ └──────────┘  └───────┘└───────┘  └──────┘└─┘└───
typ  ─┘   └────┘   └─┘ └──────┘└──┘ └──────────┘  └───────┘└───────┘  └──────┘└─┘└───
doc  ─┘   └────┘    └─┘ └──────┘                            └───────┘  └──────┘   └───
txt  ─┘   └────┘    └─┘ └──────┘                            └───────┘  └──────┘   └───
par  ─┘   └────┘    └─┘ └──────┘                            └───────┘  └──────┘   └───
pid  ─┘   └────┘    └─┘ └──────┘                            └───────┘  └──────┘   └───
st   ──────────────────────────────────────────────────────────────────────────────────────
304    λ ⟨⟨f, hf⟩⟩, cantor_injective (λ s, f (λ a, ⟨s a⟩)) $
id                 └──────────────┘
src  ─┘ └┘  └┘  └──┘└──────────────┘  └──┘   └──┘   └──┘ 
typ  ─┘ └┘ └┘  └──┘└──────────────┘  └──┘   └──┘   └──┘ 
doc  ─┘ └┘  └┘  └──┘                  └──┘   └──┘   └──┘ 
txt  ─┘ └┘  └┘  └──┘                  └──┘   └──┘   └──┘ 
par  ─┘ └┘  └┘  └──┘                  └──┘   └──┘   └──┘ 
pid  ─┘ └┘  └┘  └──┘                  └──┘   └──┘   └──┘ 
st   ────────────────────────────────────────────────────────
305      λ s t h, by funext a; injection congr_fun (hf h) a⟩
id                                       └───────┘  └┘   
src  ───┘ └──────┘  └──────┘└┘└────────┘└───────┘    └┘ └─
typ  ───┘ └──────┘  └──────┘└┘└────────┘└───────┘ └┘└┘└─
doc  ───┘ └──────┘  └──────┘└┘└────────┘             └┘ └─
txt  ───┘ └──────┘  └──────┘└┘└────────┘             └┘ └─
par  ───┘ └──────┘  └──────┘└┘└────────┘             └┘ └─
pid  ───┘ └──────┘  └───────────────────┘             └┘ 
st   ──────────────┘└─────────────────────────────────────┘└─
306  
src  
typ  
doc  
txt  
par  
pid  
st   
307  instance : no_top_order cardinal.{u} :=
id              └──────────┘ └──────┘
src             └──────────┘ └──────┘
typ             └──────────┘ └──────┘
doc             └──────────┘ └──────┘
308  { no_top := λ a, ⟨_, cantor a⟩, ..cardinal.linear_order }
id                       └────┘      └───────────────────┘
src                       └────┘       └───────────────────┘
typ                      └────┘      └───────────────────┘
309  
310  /-- The minimum cardinal in a family of cardinals (the existence
311    of which is provided by `injective_min`). -/
312  noncomputable def min {ι} (I : nonempty ι) (f : ι → cardinal) : cardinal :=
id                                  └──────┘           └──────┘    └──────┘
src                                 └──────┘             └──────┘    └──────┘
typ                                 └──────┘           └──────┘    └──────┘
doc                                                      └──────┘    └──────┘
313  f $ classical.some $
id      └────────────┘
src      └────────────┘
typ     └────────────┘
314  @embedding.injective_min _ (λ i, (f i).out) I
id    └─────────────────────┘           └─┘   
src   └─────────────────────┘              └─┘
typ   └─────────────────────┘           └─┘   
doc                                        └─┘
315  
316  theorem min_eq {ι} (I) (f : ι → cardinal) : ∃ i, min I f = f i :=
id                                  └──────┘      └─┘     
src                                  └──────┘       └─┘     
typ                                 └──────┘      └─┘     
doc                                  └──────┘         └─┘
317  ⟨_, rfl⟩
id       └─┘
src      └─┘
typ      └─┘
318  
319  theorem min_le {ι I} (f : ι → cardinal) (i) : min I f ≤ f i :=
id                                └──────┘        └─┘     
src                                └──────┘        └─┘     
typ                               └──────┘        └─┘     
doc                                └──────┘        └─┘
320  by rw [← mk_out (min I f), ← mk_out (f i)]; exact
id            └────┘  └─┘       └────┘   
src     └────┘└────┘ └─┘  └───┘└────┘   └┘  └────┘
typ     └────┘└────┘ └─┘└───┘└────┘ └┘  └────┘
doc     └────┘       └─┘  └───┘         └┘  └────┘
txt     └────┘            └───┘         └┘  └────┘
par     └────┘            └───┘         └┘  └────┘
pid       └──┘            └───┘         └┘       
st     └─────────────────────┘└──────────────┘└───────
321  let ⟨g⟩ := classical.some_spec
id             └─────────────────┘
src       └───┘└─────────────────┘
typ      └───┘└─────────────────┘
doc       └───┘                   
txt       └───┘                   
par       └───┘                   
pid       └───┘                   
st   ───────────────────────────────
322    (@embedding.injective_min _ (λ i, (f i).out) I) in
id       └─────────────────────┘                   
src  ─┘  └─────────────────────┘└─┘  └──┘   └─────┘ └───┘
typ  ─┘  └─────────────────────┘└─┘  └──┘  └─────┘└───┘
doc  ─┘                         └─┘  └──┘   └─────┘ └───┘
txt  ─┘                         └─┘  └──┘   └─────┘ └───┘
par  ─┘                         └─┘  └──┘   └─────┘ └───┘
pid  ─┘                         └─┘  └──┘   └─────┘ └───┘
st   ─────────────────────────────────────────────────────
323  ⟨g i⟩
id      
src     └─
typ    └─
doc     └─
txt     └─
par     └─
pid     
st   ──────
324  
src  
typ  
doc  
txt  
par  
pid  
st   
325  theorem le_min {ι I} {f : ι → cardinal} {a} : a ≤ min I f ↔ ∀ i, a ≤ f i :=
id                                └──────┘          └─┘           
src                                └──────┘           └─┘             
typ                               └──────┘          └─┘           
doc                                └──────┘            └─┘
326  ⟨λ h i, le_trans h (min_le _ _),
id         └──────┘   └────┘
src          └──────┘    └────┘
typ        └──────┘   └────┘
327   λ h, let ⟨i, e⟩ := min_eq I f in e.symm ▸ h i⟩
id        └─┘         └────┘       └───┘  
src                      └────┘         └───┘ 
typ       └─┘         └────┘       └───┘  
328  
329  protected theorem wf : @well_founded cardinal.{u} (<) :=
id                           └──────────┘ └──────┘     
src                          └──────────┘ └──────┘     
typ                          └──────────┘ └──────┘     
doc                                       └──────┘
330  ⟨λ a, classical.by_contradiction $ λ h,
id        └────────────────────────┘     
src        └────────────────────────┘
typ       └────────────────────────┘     
331    let ι := {c :cardinal // ¬ acc (<) c},
id     └─┘        └──────┘     └─┘    
src                └──────┘     └─┘ 
typ    └─┘        └──────┘     └─┘    
doc                 └──────┘
332        f : ι → cardinal := subtype.val,
id               └──────┘    └─────────┘
src                └──────┘    └─────────┘
typ              └──────┘    └─────────┘
doc                └──────┘
333        ⟨⟨c, hc⟩, hi⟩ := @min_eq ι ⟨⟨_, h⟩⟩ f in
id              └┘           └────┘          
src                          └────┘
typ             └┘           └────┘          
334      hc (acc.intro _ (λ j ⟨_, h'⟩,
id           └───────┘          └┘
src          └───────┘
typ          └───────┘          └┘
335        classical.by_contradiction $ λ hj, h' $
id         └────────────────────────┘     └┘
src        └────────────────────────┘
typ        └────────────────────────┘     └┘
336        by have := min_le f ⟨j, hj⟩; rwa hi at this))⟩
id                    └────┘     └┘       └┘
src           └──────┘└────┘   └┘    └──┘  └──────┘
typ           └──────┘└────┘ └┘└┘  └──┘└┘└──────┘
doc           └──────┘         └┘    └──┘  └──────┘
txt           └──────┘         └┘    └──┘  └──────┘
par           └──────┘         └┘    └──┘  └──────┘
pid           └───┘└─┘         └┘         └──────┘
st           └─────────────────────────────┘└┘└──────┘
337  
338  instance has_wf : @has_well_founded cardinal.{u} := ⟨(<), cardinal.wf⟩
id                      └──────────────┘ └──────┘             └─────────┘
src                     └──────────────┘ └──────┘             └─────────┘
typ                     └──────────────┘ └──────┘             └─────────┘
doc                                      └──────┘
339  
340  instance wo : @is_well_order cardinal.{u} (<) := ⟨cardinal.wf⟩
id                  └───────────┘ └──────┘            └─────────┘
src                 └───────────┘ └──────┘            └─────────┘
typ                 └───────────┘ └──────┘            └─────────┘
doc                 └───────────┘ └──────┘
341  
342  /-- The successor cardinal - the smallest cardinal greater than
343    `c`. This is not the same as `c + 1` except in the case of finite `c`. -/
344  noncomputable def succ (c : cardinal) : cardinal :=
id                               └──────┘    └──────┘
src                              └──────┘    └──────┘
typ                              └──────┘    └──────┘
doc                              └──────┘    └──────┘
345  @min {c' // c < c'} ⟨⟨_, cantor _⟩⟩ subtype.val
id    └─┘ └┘      └┘       └────┘     └─────────┘
src   └─┘                   └────┘     └─────────┘
typ   └─┘ └┘      └┘       └────┘     └─────────┘
doc   └─┘
346  
347  theorem lt_succ_self (c : cardinal) : c < succ c :=
id                             └──────┘      └──┘ 
src                            └──────┘       └──┘
typ                            └──────┘      └──┘ 
doc                            └──────┘        └──┘
348  by cases min_eq _ _ with s e; rw [succ, e]; exact s.2
id            └────┘                   └──┘           
src     └────┘└────┘└───────────┘  └──┘└──┘└┘   └────┘ └──
typ     └────┘└────┘└───────────┘  └──┘└──┘└┘  └────┘└──
doc     └────┘      └───────────┘  └──┘└──┘└┘   └────┘ └──
txt     └────┘      └───────────┘  └──┘    └┘   └────┘ └──
par     └────┘      └───────────┘  └──┘    └┘   └────┘ └──
pid                └──┘└───────┘    └┘    └┘         └──
st     └──────────────────────────────┘└──┘└─┘└───────────
349  
src  
typ  
doc  
txt  
par  
pid  
st   
350  theorem succ_le {a b : cardinal} : succ a ≤ b ↔ a < b :=
id                          └──────┘    └──┘       
src                         └──────┘    └──┘         
typ                         └──────┘    └──┘       
doc                         └──────┘    └──┘
351  ⟨lt_of_lt_of_le (lt_succ_self _), λ h,
id    └────────────┘  └──────────┘       
src   └────────────┘  └──────────┘
typ   └────────────┘  └──────────┘       
352    by exact min_le _ (subtype.mk b h)⟩
id              └────┘    └────────┘  
src       └────┘└────┘└─┘ └────────┘  
typ       └────┘└────┘└─┘ └────────┘
doc       └────┘      └─┘             
txt       └────┘      └─┘             
par       └────┘      └─┘             
pid                  └─┘             
st       └──────────────────────────────┘
353  
354  theorem lt_succ {a b : cardinal} : a < succ b ↔ a ≤ b :=
id                          └──────┘      └──┘     
src                         └──────┘       └──┘      
typ                         └──────┘      └──┘     
doc                         └──────┘        └──┘
355  by rw [← not_le, succ_le, not_lt]
id            └────┘  └─────┘  └────┘
src     └────┘└────┘└┘└─────┘└┘└────┘└─
typ     └────┘└────┘└┘└─────┘└┘└────┘└─
doc     └────┘      └┘       └┘      └─
txt     └────┘      └┘       └┘      └─
par     └────┘      └┘       └┘      └─
pid       └──┘      └┘       └┘      
st     └───────────┘└───────┘└──────┘
356  
src  
typ  
doc  
txt  
par  
pid  
st   
357  theorem add_one_le_succ (c : cardinal) : c + 1 ≤ succ c :=
id                                └──────┘         └──┘ 
src                               └──────┘          └──┘
typ                               └──────┘         └──┘ 
doc                               └──────┘            └──┘
358  begin
st   └─────
359    refine quot.induction_on c (λ α, _) (lt_succ_self c),
id            └───────────────┘             └──────────┘ 
src    └─────┘└───────────────┘   └─────┘ └──────────┘ 
typ    └─────┘└───────────────┘   └─────┘ └──────────┘
doc    └─────┘                    └─────┘              
txt    └─────┘                    └─────┘              
par    └─────┘                    └─────┘              
pid                              └─────┘              
st   ─────────────────────────────────────────────────────┘└─
360    refine quot.induction_on (succ (quot.mk setoid.r α)) (λ β h, _),
id            └───────────────┘  └──┘  └─────┘ └──────┘ 
src    └─────┘└───────────────┘ └──┘        └──────┘ └─┘  └──────┘
typ    └─────┘└───────────────┘ └──┘ └─────┘└──────┘└─┘  └──────┘
doc    └─────┘                  └──┘                 └─┘  └──────┘
txt    └─────┘                                       └─┘  └──────┘
par    └─────┘                                       └─┘  └──────┘
pid                                                 └─┘  └──────┘
st   ────────────────────────────────────────────────────────────────┘└─
361    cases h.left with f,
id           └────┘
src    └────┘└────┘└─────┘
typ    └────┘└────┘└─────┘
doc    └────┘      └─────┘
txt    └────┘      └─────┘
par    └────┘      └─────┘
pid               └─────┘
st   ────────────────────┘└─
362    have : ¬ surjective f := λ hn,
id              └────────┘ 
src    └─────┘ └────────┘ └──┘ └────
typ    └─────┘ └────────┘└──┘ └────
doc    └─────┘            └──┘ └────
txt    └─────┘            └──┘ └────
par    └─────┘            └──┘ └────
pid    └───┘└┘            └──┘ └────
st   ─────────────────────────────────
363      ne_of_lt h (quotient.sound ⟨equiv.of_bijective ⟨f.inj, hn⟩⟩),
id       └──────┘   └────────────┘  └────────────────┘  └───┘
src  ───┘└──────┘  └────────────┘ └────────────────┘ └───┘└┘  └─┘
typ  ───┘└──────┘ └────────────┘ └────────────────┘ └───┘└┘  └─┘
doc  ───┘                                                 └┘  └─┘
txt  ───┘                                                 └┘  └─┘
par  ───┘                                                 └┘  └─┘
pid  ───┘                                                 └┘  └─┘
st   ───────────────────────────────────────────────────────────────┘└─
364    cases classical.not_forall.1 this with b nex,
id           └──────────────────┘   └──┘
src    └────┘└──────────────────┘└─┘    └─────────┘
typ    └────┘└──────────────────┘└─┘└──┘└─────────┘
doc    └────┘                    └─┘    └─────────┘
txt    └────┘                    └─┘    └─────────┘
par    └────┘                    └─┘    └─────────┘
pid                             └─┘    └─────────┘
st   ─────────────────────────────────────────────┘└─
365    refine ⟨⟨sum.rec (by exact f) _, _⟩⟩,
id              └─────┘           
src    └─────┘  └─────┘   └────┘ └──────┘
typ    └─────┘  └─────┘   └─────┘└──────┘
doc    └─────┘            └────┘ └──────┘
txt    └─────┘            └────┘ └──────┘
par    └─────┘            └─────┘ └──────┘
pid                      └─────┘ └──────┘
st   ─────────────────────┘└──────┘└──────┘└─
366    { exact λ _, b },
id                  
src      └────┘ └──┘ 
typ      └────┘ └──┘
doc      └────┘ └──┘ 
txt      └────┘ └──┘ 
par      └────┘ └──┘ 
pid            └──┘ 
st   ───┘└───────────┘└┘
367    { intros a b h, rcases a with a|⟨⟨⟨⟩⟩⟩; rcases b with b|⟨⟨⟨⟩⟩⟩,
id                                                   
src      └──────────┘  └─────┘ └────────────┘  └─────┘ └────────────┘
typ      └──────────┘  └─────┘└────────────┘  └─────┘└────────────┘
doc      └──────────┘  └─────┘ └────────────┘  └─────┘ └────────────┘
txt      └──────────┘  └─────┘ └────────────┘  └─────┘ └────────────┘
par      └──────────┘  └─────┘ └────────────┘  └─────┘ └────────────┘
pid            └────┘         └────────────┘         └────────────┘
st   ───────────────┘└──────────────────────────────────────────────┘└─
368      { rw f.inj h },
id            └───┘ 
src        └─┘└───┘ 
typ        └─┘└───┘
doc        └─┘      
txt        └─┘      
par        └─┘      
pid                
st   ─────┘└─────────┘└┘
369      { exact nex.elim ⟨_, h⟩ },
id               └──────┘     
src        └────┘└──────┘ └─┘ └┘
typ        └────┘└──────┘ └─┘└┘
doc        └────┘         └─┘ └┘
txt        └────┘         └─┘ └┘
par        └────┘         └─┘ └┘
pid                      └─┘ 
st   ─────┘└────────────────────┘└┘
370      { exact nex.elim ⟨_, h.symm⟩ },
id               └──────┘     └────┘
src        └────┘└──────┘ └─┘└────┘└┘
typ        └────┘└──────┘ └─┘└────┘└┘
doc        └────┘         └─┘      └┘
txt        └────┘         └─┘      └┘
par        └────┘         └─┘      └┘
pid                      └─┘      
st   ─────┘└─────────────────────────┘└┘
371      { refl } }
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└───
372  end
st   ──┘
373  
374  lemma succ_ne_zero (c : cardinal) : succ c ≠ 0 :=
id                           └──────┘    └──┘  
src                          └──────┘    └──┘   
typ                          └──────┘    └──┘  
doc                          └──────┘    └──┘
375  by { rw [←pos_iff_ne_zero, lt_succ], apply zero_le }
id             └─────────────┘  └─────┘         └─────┘
src       └───┘└─────────────┘└┘└─────┘  └────┘└─────┘
typ       └───┘└─────────────┘└┘└─────┘  └────┘└─────┘
doc       └───┘               └┘         └────┘       
txt       └───┘               └┘         └────┘       
par       └───┘               └┘         └────┘       
pid         └─┘               └┘                     
st     └─────────────────────┘└───────┘└───────────────┘└┘
376  
377  /-- The indexed sum of cardinals is the cardinality of the
378    indexed disjoint union, i.e. sigma type. -/
379  def sum {ι} (f : ι → cardinal) : cardinal := mk Σ i, (f i).out
id                       └──────┘    └──────┘    └┘      └─┘
src                       └──────┘    └──────┘    └┘         └─┘
typ                      └──────┘    └──────┘    └┘      └─┘
doc                       └──────┘    └──────┘    └┘           └─┘
380  
381  theorem le_sum {ι} (f : ι → cardinal) (i) : f i ≤ sum f :=
id                              └──────┘           └─┘ 
src                              └──────┘             └─┘
typ                             └──────┘           └─┘ 
doc                              └──────┘              └─┘
382  by rw ← quotient.out_eq (f i); exact
id           └─────────────┘   
src     └───┘└─────────────┘     └────┘
typ     └───┘└─────────────┘   └────┘
doc     └───┘                    └────┘
txt     └───┘                    └────┘
par     └───┘                    └────┘
pid       └─┘                         
st     └──────────────────────────────────
383  ⟨⟨λ a, ⟨i, a⟩, λ a b h, eq_of_heq $ by injection h⟩⟩
id                          └───────┘                
src     └──┘  └┘ └─┘ └──────┘└───────┘   └────────┘ └──
typ     └──┘ └┘ └─┘ └──────┘└───────┘   └────────┘└──
doc     └──┘  └┘ └─┘ └──────┘            └────────┘ └──
txt     └──┘  └┘ └─┘ └──────┘            └────────┘ └──
par     └──┘  └┘ └─┘ └──────┘            └────────┘ └──
pid     └──┘  └┘ └─┘ └──────┘            └─────────┘ └┘
st   ─────────────────────────────────────┘└──────────┘└──
384  
src  
typ  
doc  
txt  
par  
pid  
st   
385  @[simp] theorem sum_mk {ι} (f : ι → Type*) : sum (λ i, mk (f i)) = mk (Σ i, f i) :=
id                                               └─┘      └┘       └┘     
src                                               └─┘       └┘         └┘    
typ                                              └─┘      └┘       └┘     
doc    └──┘                                       └─┘       └┘          └┘
386  quot.sound ⟨equiv.sigma_congr_right $ λ i,
id   └────────┘  └─────────────────────┘     
src  └────────┘  └─────────────────────┘
typ  └────────┘  └─────────────────────┘     
387    classical.choice $ quotient.exact $ quot.out_eq $ mk (f i)⟩
id     └──────────────┘   └────────────┘   └─────────┘   └┘   
src    └──────────────┘   └────────────┘   └─────────┘   └┘
typ    └──────────────┘   └────────────┘   └─────────┘   └┘   
doc                                                      └┘
388  
389  theorem sum_const (ι : Type u) (a : cardinal.{u}) : sum (λ _:ι, a) = mk ι * a :=
id                                       └──────┘        └─┘           └┘   
src                                      └──────┘        └─┘             └┘   
typ                                      └──────┘        └─┘           └┘   
doc                                      └──────┘        └─┘              └┘
390  quotient.induction_on a $ λ α, by simp; exact
id   └───────────────────┘      
src  └───────────────────┘             └──┘  └─────
typ  └───────────────────┘           └──┘  └─────
doc                                    └──┘  └─────
txt                                    └──┘  └─────
par                                    └──┘  └─────
pid                                               
st                                    └────────────
391    quotient.sound ⟨equiv.sigma_equiv_prod _ _⟩
id     └────────────┘  └────────────────────┘
src  ─┘└────────────┘ └────────────────────┘└─────
typ  ─┘└────────────┘ └────────────────────┘└─────
doc  ─┘                                     └─────
txt  ─┘                                     └─────
par  ─┘                                     └─────
pid  ─┘                                     └───┘
st   ──────────────────────────────────────────────
392  
src  
typ  
doc  
txt  
par  
pid  
st   
393  theorem sum_le_sum {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=
id                                    └──────┘                   └─┘   └─┘ 
src                                    └──────┘                        └─┘    └─┘
typ                                   └──────┘                   └─┘   └─┘ 
doc                                    └──────┘                         └─┘     └─┘
394  ⟨embedding.sigma_congr_right $ λ i, classical.choice $
id    └─────────────────────────┘       └──────────────┘
src   └─────────────────────────┘        └──────────────┘
typ   └─────────────────────────┘       └──────────────┘
395    by have := H i; rwa [← quot.out_eq (f i), ← quot.out_eq (g i)] at this⟩
id                          └─────────┘        └─────────┘   
src       └──────┘    └─────┘└─────────┘   └───┘└─────────┘   └────────┘
typ       └──────┘  └─────┘└─────────┘ └───┘└─────────┘ └────────┘
doc       └──────┘    └─────┘              └───┘              └────────┘
txt       └──────┘    └─────┘              └───┘              └────────┘
par       └──────┘    └─────┘              └───┘              └────────┘
pid       └───┘└─┘       └──┘              └───┘              └┘└──────┘
st       └─────────────────┘└─────────────────┘└───────────────────┘└──────┘
396  
397  /-- The indexed supremum of cardinals is the smallest cardinal above
398    everything in the family. -/
399  noncomputable def sup {ι} (f : ι → cardinal) : cardinal :=
id                                     └──────┘    └──────┘
src                                     └──────┘    └──────┘
typ                                    └──────┘    └──────┘
doc                                     └──────┘    └──────┘
400  @min {c // ∀ i, f i ≤ c} ⟨⟨sum f, le_sum f⟩⟩ (λ a, a.1)
id    └─┘                └─┘   └────┘         
src   └─┘                     └─┘    └────┘            
typ   └─┘                └─┘   └────┘         
doc   └─┘                       └─┘
401  
402  theorem le_sup {ι} (f : ι → cardinal) (i) : f i ≤ sup f :=
id                              └──────┘           └─┘ 
src                              └──────┘             └─┘
typ                             └──────┘           └─┘ 
doc                              └──────┘              └─┘
403  by dsimp [sup]; cases min_eq _ _ with c hc; rw hc; exact c.2 i
id             └─┘         └────┘                   └┘           
src     └─────┘└─┘  └────┘└────┘└────────────┘  └─┘    └────┘ └─┘ 
typ     └─────┘└─┘  └────┘└────┘└────────────┘  └─┘└┘  └────┘└─┘
doc     └─────┘└─┘  └────┘      └────────────┘  └─┘    └────┘ └─┘ 
txt     └─────┘     └────┘      └────────────┘  └─┘    └────┘ └─┘ 
par     └─────┘     └────┘      └────────────┘  └─┘    └────┘ └─┘ 
pid                          └──┘└────────┘              └─┘ 
st     └───────────────────────────────────────────┘└┘└─────────────
404  
src  
typ  
doc  
txt  
par  
pid  
st   
405  theorem sup_le {ι} {f : ι → cardinal} {a} : sup f ≤ a ↔ ∀ i, f i ≤ a :=
id                              └──────┘        └─┘            
src                              └──────┘        └─┘                
typ                             └──────┘        └─┘            
doc                              └──────┘        └─┘
406  ⟨λ h i, le_trans (le_sup _ _) h,
id         └──────┘  └────┘      
src          └──────┘  └────┘
typ        └──────┘  └────┘      
407   λ h, by dsimp [sup]; change a with (⟨a, h⟩:subtype _).1; apply min_le⟩
id                  └─┘                      └─────┘             └────┘
src           └─────┘└─┘  └─────┘ └────┘   └┘ └┘└─────┘└───┘  └────┘└────┘
typ          └─────┘└─┘  └─────┘└────┘  └┘└┘└─────┘└───┘  └────┘└────┘
doc           └─────┘└─┘  └─────┘ └────┘   └┘ └┘       └───┘  └────┘
txt           └─────┘     └─────┘ └────┘   └┘ └┘       └───┘  └────┘
par           └─────┘     └─────┘ └────┘   └┘ └┘       └───┘  └────┘
pid                            └────┘   └┘ └┘       └─┘└┘       
st           └────────────────────────────────────────────────────────────┘
408  
409  theorem sup_le_sup {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sup f ≤ sup g :=
id                                    └──────┘                   └─┘   └─┘ 
src                                    └──────┘                        └─┘    └─┘
typ                                   └──────┘                   └─┘   └─┘ 
doc                                    └──────┘                         └─┘     └─┘
410  sup_le.2 $ λ i, le_trans (H i) (le_sup _ _)
id   └────┘        └──────┘      └────┘
src  └────┘         └──────┘        └────┘
typ  └────┘        └──────┘      └────┘
411  
412  theorem sup_le_sum {ι} (f : ι → cardinal) : sup f ≤ sum f :=
id                                  └──────┘    └─┘   └─┘ 
src                                  └──────┘    └─┘    └─┘
typ                                 └──────┘    └─┘   └─┘ 
doc                                  └──────┘    └─┘     └─┘
413  sup_le.2 $ le_sum _
id   └────┘    └────┘
src  └────┘    └────┘
typ  └────┘    └────┘
414  
415  theorem sum_le_sup {ι : Type u} (f : ι → cardinal.{u}) : sum f ≤ mk ι * sup.{u u} f :=
id                                           └──────┘        └─┘   └┘   └─┘       
src                                           └──────┘        └─┘    └┘    └─┘
typ                                          └──────┘        └─┘   └┘   └─┘       
doc                                           └──────┘        └─┘     └┘     └─┘
416  by rw ← sum_const; exact sum_le_sum _ _ (le_sup _)
id           └───────┘        └────────┘      └────┘
src     └───┘└───────┘  └────┘└────────┘└───┘ └────┘└───
typ     └───┘└───────┘  └────┘└────────┘└───┘ └────┘└───
doc     └───┘           └────┘          └───┘       └───
txt     └───┘           └────┘          └───┘       └───
par     └───┘           └────┘          └───┘       └───
pid       └─┘                          └───┘       └─┘
st     └────────────────────────────────────────────────
417  
src  
typ  
doc  
txt  
par  
pid  
st   
418  theorem sup_eq_zero {ι} {f : ι → cardinal} (h : ι → false) : sup f = 0 :=
id                                   └──────┘          └───┘    └─┘  
src                                   └──────┘           └───┘    └─┘   
typ                                  └──────┘          └───┘    └─┘  
doc                                   └──────┘                    └─┘
419  by { rw [←le_zero, sup_le], intro x, exfalso, exact h x }
id             └─────┘  └────┘                            
src       └───┘└─────┘└┘└────┘  └─────┘  └─────┘  └────┘  
typ       └───┘└─────┘└┘└────┘  └─────┘  └─────┘  └────┘
doc       └───┘       └┘        └─────┘  └─────┘  └────┘  
txt       └───┘       └┘        └─────┘  └─────┘  └────┘  
par       └───┘       └┘        └─────┘  └─────┘  └────┘  
pid         └─┘       └┘             └┘                  
st     └─────────────┘└──────┘└────────┘└───────┘└──────────┘└┘
420  
421  /-- The indexed product of cardinals is the cardinality of the Pi type
422    (dependent product). -/
423  def prod {ι : Type u} (f : ι → cardinal) : cardinal := mk (Π i, (f i).out)
id                                 └──────┘    └──────┘    └┘         └─┘
src                                 └──────┘    └──────┘    └┘            └─┘
typ                                └──────┘    └──────┘    └┘         └─┘
doc                                 └──────┘    └──────┘    └┘            └─┘
424  
425  @[simp] theorem prod_mk {ι} (f : ι → Type*) : prod (λ i, mk (f i)) = mk (Π i, f i) :=
id                                                └──┘      └┘       └┘       
src                                                └──┘       └┘         └┘
typ                                               └──┘      └┘       └┘       
doc    └──┘                                        └──┘       └┘          └┘
426  quot.sound ⟨equiv.Pi_congr_right $ λ i,
id   └────────┘  └──────────────────┘     
src  └────────┘  └──────────────────┘
typ  └────────┘  └──────────────────┘     
427    classical.choice $ quotient.exact $ mk_out $ mk (f i)⟩
id     └──────────────┘   └────────────┘   └────┘   └┘   
src    └──────────────┘   └────────────┘   └────┘   └┘
typ    └──────────────┘   └────────────┘   └────┘   └┘   
doc                                                 └┘
428  
429  theorem prod_const (ι : Type u) (a : cardinal.{u}) : prod (λ _:ι, a) = a ^ mk ι :=
id                                        └──────┘        └──┘             └┘ 
src                                       └──────┘        └──┘                └┘
typ                                       └──────┘        └──┘             └┘ 
doc                                       └──────┘        └──┘                 └┘
430  quotient.induction_on a $ by simp
id   └───────────────────┘ 
src  └───────────────────┘        └────
typ  └───────────────────┘       └────
doc                               └────
txt                               └────
par                               └────
pid                                   
st                               └─────
431  
src  
typ  
doc  
txt  
par  
pid  
st   
432  theorem prod_le_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : prod f ≤ prod g :=
id                                      └──────┘                   └──┘   └──┘ 
src                                      └──────┘                        └──┘    └──┘
typ                                     └──────┘                   └──┘   └──┘ 
doc                                      └──────┘                         └──┘     └──┘
433  ⟨embedding.Pi_congr_right $ λ i, classical.choice $
id    └──────────────────────┘       └──────────────┘
src   └──────────────────────┘        └──────────────┘
typ   └──────────────────────┘       └──────────────┘
434    by have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this⟩
id                          └────┘        └────┘   
src       └──────┘    └─────┘└────┘   └───┘└────┘   └────────┘
typ       └──────┘  └─────┘└────┘ └───┘└────┘ └────────┘
doc       └──────┘    └─────┘         └───┘         └────────┘
txt       └──────┘    └─────┘         └───┘         └────────┘
par       └──────┘    └─────┘         └───┘         └────────┘
pid       └───┘└─┘       └──┘         └───┘         └┘└──────┘
st       └─────────────────┘└────────────┘└──────────────┘└──────┘
435  
436  theorem prod_ne_zero {ι} (f : ι → cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0 :=
id                                    └──────┘    └──┘            
src                                    └──────┘    └──┘                
typ                                   └──────┘    └──┘            
doc                                    └──────┘    └──┘
437  begin
st   └─────
438    conv in (f _) {rw ← mk_out (f i)},
id                        └────┘   
src    └──────┘  └───┘└───┘└────┘   
typ    └──────┘ └───┘└───┘└────┘ 
txt    └──────┘  └───┘└───┘         
par    └──────┘  └───┘└───┘         
pid        └─┘  └─┘└─────┘         └┘
st   ────────────────┘└───────────────┘└┘
439    simp [prod, ne_zero_iff_nonempty, -mk_out, -ne.def],
id           └──┘  └──────────────────┘
src    └────┘└──┘└┘└──────────────────┘└─────────────────┘
typ    └────┘└──┘└┘└──────────────────┘└─────────────────┘
doc    └────┘└──┘└┘                    └─────────────────┘
txt    └────┘    └┘                    └─────────────────┘
par    └────┘    └┘                    └─────────────────┘
pid            └┘                    └─────────────────┘
st   ────────────────────────────────────────────────────┘└─
440    exact ⟨λ ⟨F⟩ i, ⟨F i⟩, λ h, ⟨λ i, classical.choice (h i)⟩⟩,
id                                      └──────────────┘
src    └────┘  └┘ └───┘   └─┘ └──┘  └──┘└──────────────┘   └─┘
typ    └────┘  └┘└───┘   └─┘ └──┘  └──┘└──────────────┘   └─┘
doc    └────┘  └┘ └───┘   └─┘ └──┘  └──┘                   └─┘
txt    └────┘  └┘ └───┘   └─┘ └──┘  └──┘                   └─┘
par    └────┘  └┘ └───┘   └─┘ └──┘  └──┘                   └─┘
pid           └┘ └───┘   └─┘ └──┘  └──┘                   └─┘
st   ───────────────────────────────────────────────────────────┘└─
441  end
st   ──┘
442  
443  theorem prod_eq_zero {ι} (f : ι → cardinal) : prod f = 0 ↔ ∃ i, f i = 0 :=
id                                    └──────┘    └──┘          
src                                    └──────┘    └──┘              
typ                                   └──────┘    └──┘          
doc                                    └──────┘    └──┘
444  not_iff_not.1 $ by simpa using prod_ne_zero f
id   └─────────┘                   └──────────┘ 
src  └─────────┘       └──────────┘└──────────┘ 
typ  └─────────┘       └──────────┘└──────────┘
doc                     └──────────┘             
txt                     └──────────┘             
par                     └──────────┘             
pid                          └────┘             
st                     └───────────────────────────
445  
src  
typ  
doc  
txt  
par  
pid  
st   
446  /-- The universe lift operation on cardinals. You can specify the universes explicitly with
447    `lift.{u v} : cardinal.{u} → cardinal.{max u v}` -/
448  def lift (c : cardinal.{u}) : cardinal.{max u v} :=
id                 └──────┘        └──────┘
src                └──────┘        └──────┘
typ                └──────┘        └──────┘
doc                └──────┘        └──────┘
449  quotient.lift_on c (λ α, ⟦ulift α⟧) $ λ α β ⟨e⟩,
id   └──────────────┘       └───┘         
src  └──────────────┘         └───┘  
typ  └──────────────┘       └───┘         
doc                            └───┘
450  quotient.sound ⟨equiv.ulift.trans $ e.trans equiv.ulift.symm⟩
id   └────────────┘  └─────────┘└────┘    └────┘ └─────────┘└───┘
src  └────────────┘  └─────────┘└────┘    └────┘ └─────────┘└───┘
typ  └────────────┘  └─────────┘└────┘    └────┘ └─────────┘└───┘
451  
452  theorem lift_mk (α) : lift.{u v} (mk α) = mk (ulift.{v u} α) := rfl
id                         └──┘        └┘    └┘  └───┘            └─┘
src                        └──┘        └┘     └┘  └───┘             └─┘
typ                        └──┘        └┘    └┘  └───┘            └─┘
doc                        └──┘        └┘      └┘  └───┘
453  
454  theorem lift_umax : lift.{u (max u v)} = lift.{u v} :=
id                       └──┘                └──┘
src                      └──┘                └──┘
typ                      └──┘                └──┘
doc                      └──┘                 └──┘
455  funext $ λ a, quot.induction_on a $ λ α,
id   └────┘       └───────────────┘      
src  └────┘        └───────────────┘
typ  └────┘       └───────────────┘      
456  quotient.sound ⟨equiv.ulift.trans equiv.ulift.symm⟩
id   └────────────┘  └─────────┘└────┘ └─────────┘└───┘
src  └────────────┘  └─────────┘└────┘ └─────────┘└───┘
typ  └────────────┘  └─────────┘└────┘ └─────────┘└───┘
457  
458  theorem lift_id' (a : cardinal) : lift a = a :=
id                         └──────┘    └──┘   
src                        └──────┘    └──┘   
typ                        └──────┘    └──┘   
doc                        └──────┘    └──┘
459  quot.induction_on a $ λ α, quot.sound ⟨equiv.ulift⟩
id   └───────────────┘        └────────┘  └─────────┘
src  └───────────────┘          └────────┘  └─────────┘
typ  └───────────────┘        └────────┘  └─────────┘
460  
461  @[simp] theorem lift_id : ∀ a, lift.{u u} a = a := lift_id'.{u u}
id                                 └──┘             └──────┘
src                                 └──┘               └──────┘
typ                                └──┘             └──────┘
doc    └──┘                         └──┘
462  
463  @[simp] theorem lift_lift (a : cardinal) : lift.{(max u v) w} (lift.{u v} a) = lift.{u (max v w)} a :=
id                                  └──────┘    └──┘                └──┘          └──┘               
src                                 └──────┘    └──┘                └──┘           └──┘
typ                                 └──────┘    └──┘                └──┘          └──┘               
doc    └──┘                         └──────┘    └──┘                └──┘            └──┘
464  quot.induction_on a $ λ α,
id   └───────────────┘      
src  └───────────────┘
typ  └───────────────┘      
465  quotient.sound ⟨equiv.ulift.trans $ equiv.ulift.trans equiv.ulift.symm⟩
id   └────────────┘  └─────────┘└────┘   └─────────┘└────┘ └─────────┘└───┘
src  └────────────┘  └─────────┘└────┘   └─────────┘└────┘ └─────────┘└───┘
typ  └────────────┘  └─────────┘└────┘   └─────────┘└────┘ └─────────┘└───┘
466  
467  theorem lift_mk_le {α : Type u} {β : Type v} :
468    lift.{u (max v w)} (mk α) ≤ lift.{v (max u w)} (mk β) ↔ nonempty (α ↪ β) :=
id     └──┘                └┘    └──┘                └┘    └──────┘    
src    └──┘                └┘     └──┘                └┘     └──────┘    
typ    └──┘                └┘    └──┘                └┘    └──────┘    
doc    └──┘                └┘      └──┘                └┘
469  ⟨λ ⟨f⟩, ⟨embedding.congr equiv.ulift equiv.ulift f⟩,
id          └─────────────┘ └─────────┘ └─────────┘
src           └─────────────┘ └─────────┘ └─────────┘
typ         └─────────────┘ └─────────┘ └─────────┘
470   λ ⟨f⟩, ⟨embedding.congr equiv.ulift.symm equiv.ulift.symm f⟩⟩
id          └─────────────┘ └─────────┘└───┘ └─────────┘└───┘
src           └─────────────┘ └─────────┘└───┘ └─────────┘└───┘
typ         └─────────────┘ └─────────┘└───┘ └─────────┘└───┘
471  
472  theorem lift_mk_eq {α : Type u} {β : Type v} :
473    lift.{u (max v w)} (mk α) = lift.{v (max u w)} (mk β) ↔ nonempty (α ≃ β) :=
id     └──┘                └┘    └──┘                └┘    └──────┘    
src    └──┘                └┘     └──┘                └┘     └──────┘    
typ    └──┘                └┘    └──┘                └┘    └──────┘    
doc    └──┘                └┘      └──┘                └┘                  
474  quotient.eq.trans
id   └─────────┘└────┘
src  └─────────┘└────┘
typ  └─────────┘└────┘
475  ⟨λ ⟨f⟩, ⟨equiv.ulift.symm.trans $ f.trans equiv.ulift⟩,
id          └─────────┘└───┘└────┘    └────┘ └─────────┘
src           └─────────┘└───┘└────┘    └────┘ └─────────┘
typ         └─────────┘└───┘└────┘    └────┘ └─────────┘
476   λ ⟨f⟩, ⟨equiv.ulift.trans $ f.trans equiv.ulift.symm⟩⟩
id          └─────────┘└────┘    └────┘ └─────────┘└───┘
src           └─────────┘└────┘    └────┘ └─────────┘└───┘
typ         └─────────┘└────┘    └────┘ └─────────┘└───┘
477  
478  @[simp] theorem lift_le {a b : cardinal} : lift a ≤ lift b ↔ a ≤ b :=
id                                  └──────┘    └──┘   └──┘     
src                                 └──────┘    └──┘    └──┘      
typ                                 └──────┘    └──┘   └──┘     
doc    └──┘                         └──────┘    └──┘     └──┘
479  quotient.induction_on₂ a b $ λ α β,
id   └────────────────────┘        
src  └────────────────────┘
typ  └────────────────────┘        
480  by rw ← lift_umax; exact lift_mk_le
id           └───────┘        └────────┘
src     └───┘└───────┘  └────┘└────────┘
typ     └───┘└───────┘  └────┘└────────┘
doc     └───┘           └────┘          
txt     └───┘           └────┘          
par     └───┘           └────┘          
pid       └─┘                          
st     └─────────────────────────────────
481  
src  
typ  
doc  
txt  
par  
pid  
st   
482  @[simp] theorem lift_inj {a b : cardinal} : lift a = lift b ↔ a = b :=
id                                   └──────┘    └──┘   └──┘     
src                                  └──────┘    └──┘    └──┘      
typ                                  └──────┘    └──┘   └──┘     
doc    └──┘                          └──────┘    └──┘     └──┘
483  by simp [le_antisymm_iff]
id            └─────────────┘
src     └────┘└─────────────┘└─
typ     └────┘└─────────────┘└─
doc     └────┘               └─
txt     └────┘               └─
par     └────┘               └─
pid                        
st     └───────────────────────
484  
src  
typ  
doc  
txt  
par  
pid  
st   
485  @[simp] theorem lift_lt {a b : cardinal} : lift a < lift b ↔ a < b :=
id                                  └──────┘    └──┘   └──┘     
src                                 └──────┘    └──┘    └──┘      
typ                                 └──────┘    └──┘   └──┘     
doc    └──┘                         └──────┘    └──┘     └──┘
486  by simp [lt_iff_le_not_le, -not_le]
id            └──────────────┘
src     └────┘└──────────────┘└──────────
typ     └────┘└──────────────┘└──────────
doc     └────┘                └──────────
txt     └────┘                └──────────
par     └────┘                └──────────
pid                         └────────┘
st     └─────────────────────────────────
487  
src  
typ  
doc  
txt  
par  
pid  
st   
488  @[simp] theorem lift_zero : lift 0 = 0 :=
id                               └──┘   
src                              └──┘   
typ                              └──┘   
doc    └──┘                      └──┘
489  quotient.sound ⟨equiv.ulift.trans equiv.pempty_equiv_pempty⟩
id   └────────────┘  └─────────┘└────┘ └───────────────────────┘
src  └────────────┘  └─────────┘└────┘ └───────────────────────┘
typ  └────────────┘  └─────────┘└────┘ └───────────────────────┘
490  
491  @[simp] theorem lift_one : lift 1 = 1 :=
id                              └──┘   
src                             └──┘   
typ                             └──┘   
doc    └──┘                     └──┘
492  quotient.sound ⟨equiv.ulift.trans equiv.punit_equiv_punit⟩
id   └────────────┘  └─────────┘└────┘ └─────────────────────┘
src  └────────────┘  └─────────┘└────┘ └─────────────────────┘
typ  └────────────┘  └─────────┘└────┘ └─────────────────────┘
493  
494  @[simp] theorem lift_add (a b) : lift (a + b) = lift a + lift b :=
id                                    └──┘       └──┘   └──┘ 
src                                   └──┘         └──┘    └──┘
typ                                   └──┘       └──┘   └──┘ 
doc    └──┘                           └──┘           └──┘     └──┘
495  quotient.induction_on₂ a b $ λ α β,
id   └────────────────────┘        
src  └────────────────────┘
typ  └────────────────────┘        
496  quotient.sound ⟨equiv.ulift.trans (equiv.sum_congr equiv.ulift equiv.ulift).symm⟩
id   └────────────┘  └─────────┘└────┘  └─────────────┘ └─────────┘ └─────────┘ └──┘
src  └────────────┘  └─────────┘└────┘  └─────────────┘ └─────────┘ └─────────┘ └──┘
typ  └────────────┘  └─────────┘└────┘  └─────────────┘ └─────────┘ └─────────┘ └──┘
497  
498  @[simp] theorem lift_mul (a b) : lift (a * b) = lift a * lift b :=
id                                    └──┘       └──┘   └──┘ 
src                                   └──┘         └──┘    └──┘
typ                                   └──┘       └──┘   └──┘ 
doc    └──┘                           └──┘           └──┘     └──┘
499  quotient.induction_on₂ a b $ λ α β,
id   └────────────────────┘        
src  └────────────────────┘
typ  └────────────────────┘        
500  quotient.sound ⟨equiv.ulift.trans (equiv.prod_congr equiv.ulift equiv.ulift).symm⟩
id   └────────────┘  └─────────┘└────┘  └──────────────┘ └─────────┘ └─────────┘ └──┘
src  └────────────┘  └─────────┘└────┘  └──────────────┘ └─────────┘ └─────────┘ └──┘
typ  └────────────┘  └─────────┘└────┘  └──────────────┘ └─────────┘ └─────────┘ └──┘
501  
502  @[simp] theorem lift_power (a b) : lift (a ^ b) = lift a ^ lift b :=
id                                      └──┘       └──┘   └──┘ 
src                                     └──┘         └──┘    └──┘
typ                                     └──┘       └──┘   └──┘ 
doc    └──┘                             └──┘          └──┘    └──┘
503  quotient.induction_on₂ a b $ λ α β,
id   └────────────────────┘        
src  └────────────────────┘
typ  └────────────────────┘        
504  quotient.sound ⟨equiv.ulift.trans (equiv.arrow_congr equiv.ulift equiv.ulift).symm⟩
id   └────────────┘  └─────────┘└────┘  └───────────────┘ └─────────┘ └─────────┘ └──┘
src  └────────────┘  └─────────┘└────┘  └───────────────┘ └─────────┘ └─────────┘ └──┘
typ  └────────────┘  └─────────┘└────┘  └───────────────┘ └─────────┘ └─────────┘ └──┘
505  
506  @[simp] theorem lift_two_power (a) : lift (2 ^ a) = 2 ^ lift a :=
id                                        └──┘           └──┘ 
src                                       └──┘            └──┘
typ                                       └──┘           └──┘ 
doc    └──┘                               └──┘             └──┘
507  by simp [bit0]
id            └──┘
src     └────┘└──┘└─
typ     └────┘└──┘└─
doc     └────┘    └─
txt     └────┘    └─
par     └────┘    └─
pid             
st     └────────────
508  
src  
typ  
doc  
txt  
par  
pid  
st   
509  @[simp] theorem lift_min {ι I} (f : ι → cardinal) : lift (min I f) = min I (lift ∘ f) :=
id                                          └──────┘    └──┘  └─┘     └─┘   └──┘  
src                                          └──────┘    └──┘  └─┘       └─┘    └──┘ 
typ                                         └──────┘    └──┘  └─┘     └─┘   └──┘  
doc    └──┘                                  └──────┘    └──┘  └─┘        └─┘    └──┘
510  le_antisymm (le_min.2 $ λ a, lift_le.2 $ min_le _ a) $
id   └─────────┘  └────┘        └─────┘    └────┘   
src  └─────────┘  └────┘         └─────┘    └────┘
typ  └─────────┘  └────┘        └─────┘    └────┘   
511  let ⟨i, e⟩ := min_eq I (lift ∘ f) in
id   └─┘           └────┘   └──┘  
src                └────┘    └──┘ 
typ  └─┘           └────┘   └──┘  
doc                          └──┘
512  by rw e; exact lift_le.2 (le_min.2 $ λ j, lift_le.1 $
id                            └────┘          └─────┘
src     └─┘   └────┘       └─┘ └────┘└─┘  └──┘└─────┘└─┘ 
typ     └─┘  └────┘       └─┘ └────┘└─┘  └──┘└─────┘└─┘ 
doc     └─┘   └────┘       └─┘       └─┘  └──┘       └─┘ 
txt     └─┘   └────┘       └─┘       └─┘  └──┘       └─┘ 
par     └─┘   └────┘       └─┘       └─┘  └──┘       └─┘ 
pid                      └─┘       └─┘  └──┘       └─┘ 
st     └───────────────────────────────────────────────────
513  by have := min_le (lift ∘ f) j; rwa e at this)
id              └────┘  └──┘          
src    └──────┘└────┘ └──┘ └┘ └┘└──┘ └──────┘└─
typ    └──────┘└────┘ └──┘└┘└┘└──┘└──────┘└─
doc    └──────┘       └──┘  └┘ └┘└──┘ └──────┘└─
txt    └──────┘             └┘ └┘└──┘ └──────┘└─
par    └──────┘             └┘ └┘└──┘ └──────┘└─
pid    └───────┘             └┘ └────┘ └───────┘
st   ─┘└────────────────────────────────┘└──────┘└─
514  
src  
typ  
doc  
txt  
par  
pid  
st   
515  theorem lift_down {a : cardinal.{u}} {b : cardinal.{max u v}} :
id                          └──────┘           └──────┘
src                         └──────┘           └──────┘
typ                         └──────┘           └──────┘
doc                         └──────┘           └──────┘
516    b ≤ lift a → ∃ a', lift a' = b :=
id       └──┘     └┘ └──┘ └┘  
src       └──┘         └──┘    
typ      └──┘     └┘ └──┘ └┘  
doc        └──┘           └──┘
517  quotient.induction_on₂ a b $ λ α β,
id   └────────────────────┘        
src  └────────────────────┘
typ  └────────────────────┘        
518  by dsimp; rw [← lift_id (mk β), ← lift_umax, ← lift_umax.{u v}, lift_mk_le]; exact
id                   └─────┘  └┘      └───────┘    └───────┘        └────────┘
src     └───┘  └────┘└─────┘ └┘ └───┘└───────┘└──┘└───────┘└──────┘└────────┘  └────┘
typ     └───┘  └────┘└─────┘ └┘└───┘└───────┘└──┘└───────┘└──────┘└────────┘  └────┘
doc     └───┘  └────┘        └┘ └───┘         └──┘         └──────┘            └────┘
txt     └───┘  └────┘           └───┘         └──┘         └──────┘            └────┘
par     └───┘  └────┘           └───┘         └──┘         └──────┘            └────┘
pid              └──┘           └───┘         └──┘         └──────┘                 
st     └──────────┘└──────────────┘└──────────────────────────────┘└──────────┘└───────
519  λ ⟨f⟩, ⟨mk (set.range f), eq.symm $ lift_mk_eq.2
id          └┘  └───────┘     └─────┘   └────────┘
src   └┘ └─┘ └┘ └───────┘ └─┘└─────┘ └────────┘└──
typ   └┘└─┘ └┘ └───────┘ └─┘└─────┘ └────────┘└──
doc   └┘ └─┘ └┘ └───────┘ └─┘                  └──
txt   └┘ └─┘              └─┘                  └──
par   └┘ └─┘              └─┘                  └──
pid   └┘ └─┘              └─┘                  └──
st   ─────────────────────────────────────────────────
520    ⟨embedding.equiv_of_surjective
id      └───────────────────────────┘
src  ─┘ └───────────────────────────┘
typ  ─┘ └───────────────────────────┘
doc  ─┘                              
txt  ─┘                              
par  ─┘                              
pid  ─┘                              
st   ─────────────────────────────────
521      (embedding.cod_restrict _ f set.mem_range_self)
id        └────────────────────┘     └────────────────┘
src  ───┘ └────────────────────┘└─┘ └────────────────┘└─
typ  ───┘ └────────────────────┘└─┘ └────────────────┘└─
doc  ───┘ └────────────────────┘└─┘                   └─
txt  ───┘                       └─┘                   └─
par  ───┘                       └─┘                   └─
pid  ───┘                       └─┘                   └─
st   ────────────────────────────────────────────────────
522      $ λ ⟨a, ⟨b, e⟩⟩, ⟨b, subtype.eq e⟩⟩⟩
id                          └────────┘
src  ───┘  └┘ └┘  └┘ └──┘  └┘└────────┘ └───
typ  ───┘  └┘ └┘ └┘└──┘  └┘└────────┘ └───
doc  ───┘  └┘ └┘  └┘ └──┘  └┘           └───
txt  ───┘  └┘ └┘  └┘ └──┘  └┘           └───
par  ───┘  └┘ └┘  └┘ └──┘  └┘           └───
pid  ───┘  └┘ └┘  └┘ └──┘  └┘           └─┘
st   ─────────────────────────────────────────
523  
src  
typ  
doc  
txt  
par  
pid  
st   
524  theorem le_lift_iff {a : cardinal.{u}} {b : cardinal.{max u v}} :
id                            └──────┘           └──────┘
src                           └──────┘           └──────┘
typ                           └──────┘           └──────┘
doc                           └──────┘           └──────┘
525    b ≤ lift a ↔ ∃ a', lift a' = b ∧ a' ≤ a :=
id       └──┘    └┘ └──┘ └┘    └┘  
src       └──┘        └──┘           
typ      └──┘    └┘ └──┘ └┘    └┘  
doc        └──┘           └──┘
526  ⟨λ h, let ⟨a', e⟩ := lift_down h in ⟨a', e, lift_le.1 $ e.symm ▸ h⟩,
id        └─┘  └┘       └───────┘             └─────┘     └───┘  
src                       └───────┘              └─────┘     └───┘ 
typ       └─┘  └┘       └───────┘             └─────┘     └───┘  
527   λ ⟨a', e, h⟩, e ▸ lift_le.2 h⟩
id                  └─────┘
src                    └─────┘
typ                 └─────┘
528  
529  theorem lt_lift_iff {a : cardinal.{u}} {b : cardinal.{max u v}} :
id                            └──────┘           └──────┘
src                           └──────┘           └──────┘
typ                           └──────┘           └──────┘
doc                           └──────┘           └──────┘
530    b < lift a ↔ ∃ a', lift a' = b ∧ a' < a :=
id       └──┘    └┘ └──┘ └┘    └┘  
src       └──┘        └──┘           
typ      └──┘    └┘ └──┘ └┘    └┘  
doc        └──┘           └──┘
531  ⟨λ h, let ⟨a', e⟩ := lift_down (le_of_lt h) in
id        └─┘  └┘       └───────┘  └──────┘ 
src                       └───────┘  └──────┘
typ       └─┘  └┘       └───────┘  └──────┘ 
532        ⟨a', e, lift_lt.1 $ e.symm ▸ h⟩,
id                 └─────┘     └───┘  
src                └─────┘     └───┘ 
typ                └─────┘     └───┘  
533   λ ⟨a', e, h⟩, e ▸ lift_lt.2 h⟩
id                  └─────┘
src                    └─────┘
typ                 └─────┘
534  
535  @[simp] theorem lift_succ (a) : lift (succ a) = succ (lift a) :=
id                                   └──┘  └──┘    └──┘  └──┘ 
src                                  └──┘  └──┘     └──┘  └──┘
typ                                  └──┘  └──┘    └──┘  └──┘ 
doc    └──┘                          └──┘  └──┘      └──┘  └──┘
536  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
537    (le_of_not_gt $ λ h, begin
id      └──────────┘     
src     └──────────┘
typ     └──────────┘     
st                          └─────
538      rcases lt_lift_iff.1 h with ⟨b, e, h⟩,
id              └─────────┘   
src      └─────┘└─────────┘└─┘ └─────────────┘
typ      └─────┘└─────────┘└─┘└─────────────┘
doc      └─────┘           └─┘ └─────────────┘
txt      └─────┘           └─┘ └─────────────┘
par      └─────┘           └─┘ └─────────────┘
pid                       └─┘ └─────────────┘
st   ────────────────────────────────────────┘└─
539      rw [lt_succ, ← lift_le, e] at h,
id           └─────┘    └─────┘  
src      └──┘└─────┘└──┘└─────┘└┘ └────┘
typ      └──┘└─────┘└──┘└─────┘└┘└────┘
doc      └──┘       └──┘       └┘ └────┘
txt      └──┘       └──┘       └┘ └────┘
par      └──┘       └──┘       └┘ └────┘
pid        └┘       └──┘       └┘ └───┘
st   ──────────────┘└─────────┘└─┘└───┘└─
540      exact not_lt_of_le h (lt_succ_self _)
id             └──────────┘   └──────────┘
src      └────┘└──────────┘  └──────────┘└───
typ      └────┘└──────────┘ └──────────┘└───
doc      └────┘                          └───
txt      └────┘                          └───
par      └────┘                          └───
pid                                     └─┘
st   ──────────────────────────────────────────
541    end)
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
542    (succ_le.2 $ lift_lt.2 $ lt_succ_self _)
id      └─────┘    └─────┘    └──────────┘
src     └─────┘    └─────┘    └──────────┘
typ     └─────┘    └─────┘    └──────────┘
543  
544  @[simp] theorem lift_max {a : cardinal.{u}} {b : cardinal.{v}} :
id                                 └──────┘           └──────┘
src                                └──────┘           └──────┘
typ                                └──────┘           └──────┘
doc    └──┘                        └──────┘           └──────┘
545    lift.{u (max v w)} a = lift.{v (max u w)} b ↔ lift.{u v} a = lift.{v u} b :=
id     └──┘                 └──┘                 └──┘         └──┘       
src    └──┘                  └──┘                  └──┘          └──┘
typ    └──┘                 └──┘                 └──┘         └──┘       
doc    └──┘                   └──┘                   └──┘           └──┘
546  calc lift.{u (max v w)} a = lift.{v (max u w)} b
id        └──┘                 └──┘               
src       └──┘                  └──┘
typ       └──┘                 └──┘               
doc       └──┘                   └──┘
547    ↔ lift.{(max u v) w} (lift.{u v} a)
id       └──┘                └──┘       
src      └──┘                └──┘
typ      └──┘                └──┘       
doc      └──┘                └──┘
548      = lift.{(max u v) w} (lift.{v u} b) : by simp
id        └──┘                └──┘       
src       └──┘                └──┘               └────
typ       └──┘                └──┘              └────
doc        └──┘                └──┘               └────
txt                                               └────
par                                               └────
pid                                                   
st                                               └─────
549    ... ↔ lift.{u v} a = lift.{v u} b : lift_inj
id           └──┘         └──┘          └──────┘
src  ─┘      └──┘          └──┘           └──────┘
typ  ─┘      └──┘         └──┘          └──────┘
doc  ─┘      └──┘           └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
550  
551  theorem mk_prod {α : Type u} {β : Type v} :
552    mk (α × β) = lift.{u v} (mk α) * lift.{v u} (mk β) :=
id     └┘       └──┘        └┘    └──┘        └┘ 
src    └┘         └──┘        └┘     └──┘        └┘
typ    └┘       └──┘        └┘    └──┘        └┘ 
doc    └┘           └──┘        └┘      └──┘        └┘
553  quotient.sound ⟨equiv.prod_congr (equiv.ulift).symm (equiv.ulift).symm⟩
id   └────────────┘  └──────────────┘  └─────────┘ └──┘   └─────────┘ └──┘
src  └────────────┘  └──────────────┘  └─────────┘ └──┘   └─────────┘ └──┘
typ  └────────────┘  └──────────────┘  └─────────┘ └──┘   └─────────┘ └──┘
554  
555  theorem sum_const_eq_lift_mul (ι : Type u) (a : cardinal.{v}) :
id                                                   └──────┘
src                                                  └──────┘
typ                                                  └──────┘
doc                                                  └──────┘
556    sum (λ _:ι, a) = lift.{u v} (mk ι) * lift.{v u} a :=
id     └─┘           └──┘        └┘    └──┘       
src    └─┘             └──┘        └┘     └──┘
typ    └─┘           └──┘        └┘    └──┘       
doc    └─┘              └──┘        └┘      └──┘
557  begin
st   └─────
558    apply quotient.induction_on a,
id           └───────────────────┘ 
src    └────┘└───────────────────┘
typ    └────┘└───────────────────┘
doc    └────┘                     
txt    └────┘                     
par    └────┘                     
pid                              
st   ──────────────────────────────┘└─
559    intro α,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
560    simp only [cardinal.mk_def, cardinal.sum_mk, cardinal.lift_id],
id                └─────────────┘  └─────────────┘  └──────────────┘
src    └─────────┘└─────────────┘└┘└─────────────┘└┘└──────────────┘
typ    └─────────┘└─────────────┘└┘└─────────────┘└┘└──────────────┘
doc    └─────────┘               └┘               └┘                
txt    └─────────┘               └┘               └┘                
par    └─────────┘               └┘               └┘                
pid        └──┘└┘               └┘               └┘                
st   ───────────────────────────────────────────────────────────────┘└─
561    convert mk_prod using 1,
id             └─────┘
src    └──────┘└─────┘└──────┘
typ    └──────┘└─────┘└──────┘
doc    └──────┘       └──────┘
txt    └──────┘       └──────┘
par    └──────┘       └──────┘
pid                  └─────┘
st   ────────────────────────┘└─
562    exact quotient.sound ⟨equiv.sigma_equiv_prod ι α⟩,
id           └────────────┘  └────────────────────┘  
src    └────┘└────────────┘ └────────────────────┘  
typ    └────┘└────────────┘ └────────────────────┘
doc    └────┘                                       
txt    └────┘                                       
par    └────┘                                       
pid                                                
st   ──────────────────────────────────────────────────┘└─
563  end
st   ──┘
564  
565  /-- `ω` is the smallest infinite cardinal, also known as ℵ₀. -/
566  def omega : cardinal.{u} := lift (mk ℕ)
id               └──────┘        └──┘  └┘ 
src              └──────┘        └──┘  └┘ 
typ              └──────┘        └──┘  └┘ 
doc              └──────┘        └──┘  └┘
567  
568  lemma mk_nat : mk nat = omega := (lift_id _).symm
id                  └┘ └─┘  └───┘     └─────┘   └──┘
src                 └┘ └─┘  └───┘     └─────┘   └──┘
typ                 └┘ └─┘  └───┘     └─────┘   └──┘
doc                 └┘       └───┘
569  
570  theorem omega_ne_zero : omega ≠ 0 :=
id                           └───┘ 
src                          └───┘ 
typ                          └───┘ 
doc                          └───┘
571  ne_zero_iff_nonempty.2 ⟨⟨0⟩⟩
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
572  
573  theorem omega_pos : 0 < omega :=
id                          └───┘
src                         └───┘
typ                         └───┘
doc                          └───┘
574  pos_iff_ne_zero.2 omega_ne_zero
id   └─────────────┘  └───────────┘
src  └─────────────┘  └───────────┘
typ  └─────────────┘  └───────────┘
575  
576  @[simp] theorem lift_omega : lift omega = omega := lift_lift _
id                                └──┘ └───┘  └───┘    └───────┘
src                               └──┘ └───┘  └───┘    └───────┘
typ                               └──┘ └───┘  └───┘    └───────┘
doc    └──┘                       └──┘ └───┘   └───┘
577  
578  /- properties about the cast from nat -/
579  
580  @[simp] theorem mk_fin : ∀ (n : ℕ), mk (fin n) = n
id                                     └┘  └─┘    
src                                     └┘  └─┘    
typ                                    └┘  └─┘    
doc    └──┘                              └┘
581  | 0     := quotient.sound ⟨(equiv.pempty_of_not_nonempty $ λ ⟨h⟩, h.elim0)⟩
id              └────────────┘   └──────────────────────────┘         └────┘
src             └────────────┘   └──────────────────────────┘           └────┘
typ             └────────────┘   └──────────────────────────┘         └────┘
582  | (n+1) := by rw [nat.cast_succ, ← mk_fin]; exact
id                    └───────────┘    └────┘
src               └──┘└───────────┘└──┘        └─────
typ               └──┘└───────────┘└──┘└────┘  └─────
doc                └──┘             └──┘        └─────
txt                └──┘             └──┘        └─────
par                └──┘             └──┘        └─────
pid                  └┘             └──┘             
st                └────────────────┘└────────┘└───────
583    quotient.sound (fintype.card_eq.1 $ by simp)
id     └────────────┘  └─────────────┘
src  ─┘└────────────┘ └─────────────┘└─┘   └──┘└─
typ  ─┘└────────────┘ └─────────────┘└─┘   └──┘└─
doc  ─┘                              └─┘   └──┘└─
txt  ─┘                              └─┘   └──┘└─
par  ─┘                              └─┘   └──┘└─
pid  ─┘                              └─┘   └────┘
st   ───────────────────────────────────────┘└───┘└─
584  
src  
typ  
doc  
txt  
par  
pid  
st   
585  @[simp] theorem lift_nat_cast (n : ℕ) : lift n = n :=
id                                          └──┘   
src                                         └──┘   
typ                                         └──┘   
doc    └──┘                                  └──┘
586  by induction n; simp *
id                
src     └────────┘   └──────
typ     └────────┘  └──────
doc     └────────┘   └──────
txt     └────────┘   └──────
par     └────────┘   └──────
pid                     
st     └────────────────────
587  
src  
typ  
doc  
txt  
par  
pid  
st   
588  lemma lift_eq_nat_iff {a : cardinal.{u}} {n : ℕ} : lift.{u v} a = n ↔ a = n :=
id                              └──────┘               └──┘             
src                             └──────┘               └──┘               
typ                             └──────┘               └──┘             
doc                             └──────┘                └──┘
589  by rw [← lift_nat_cast.{u v} n, lift_inj]
id            └───────────┘         └──────┘
src     └────┘└───────────┘└─────┘ └┘└──────┘└─
typ     └────┘└───────────┘└─────┘└┘└──────┘└─
doc     └────┘             └─────┘ └┘        └─
txt     └────┘             └─────┘ └┘        └─
par     └────┘             └─────┘ └┘        └─
pid       └──┘             └─────┘ └┘        
st     └──────────────────────────┘└────────┘
590  
src  
typ  
doc  
txt  
par  
pid  
st   
591  lemma nat_eq_lift_eq_iff {n : ℕ} {a : cardinal.{u}} :
id                                        └──────┘
src                                       └──────┘
typ                                       └──────┘
doc                                        └──────┘
592    (n : cardinal) = lift.{u v} a ↔ (n : cardinal) = a :=
id         └──────┘   └──┘             └──────┘   
src         └──────┘   └──┘               └──────┘  
typ        └──────┘   └──┘             └──────┘   
doc         └──────┘    └──┘                └──────┘
593  by rw [← lift_nat_cast.{u v} n, lift_inj]
id            └───────────┘         └──────┘
src     └────┘└───────────┘└─────┘ └┘└──────┘└─
typ     └────┘└───────────┘└─────┘└┘└──────┘└─
doc     └────┘             └─────┘ └┘        └─
txt     └────┘             └─────┘ └┘        └─
par     └────┘             └─────┘ └┘        └─
pid       └──┘             └─────┘ └┘        
st     └──────────────────────────┘└────────┘
594  
src  
typ  
doc  
txt  
par  
pid  
st   
595  theorem lift_mk_fin (n : ℕ) : lift (mk (fin n)) = n := by simp
id                                └──┘  └┘  └─┘     
src                               └──┘  └┘  └─┘              └────
typ                               └──┘  └┘  └─┘            └────
doc                                └──┘  └┘                    └────
txt                                                            └────
par                                                            └────
pid                                                                
st                                                            └─────
596  
src  
typ  
doc  
txt  
par  
pid  
st   
597  theorem fintype_card (α : Type u) [fintype α] : mk α = fintype.card α :=
id                                      └─────┘     └┘   └──────────┘ 
src                                     └─────┘      └┘    └──────────┘
typ                                     └─────┘     └┘   └──────────┘ 
doc                                     └─────┘      └┘     └──────────┘
598  by rw [← lift_mk_fin.{u}, ← lift_id (mk α), lift_mk_eq.{u 0 u}];
id            └─────────┘        └─────┘  └┘    └────────┘
src     └────┘└─────────┘└──────┘└─────┘ └┘ └─┘└────────┘└───────┘
typ     └────┘└─────────┘└──────┘└─────┘ └┘└─┘└────────┘└───────┘
doc     └────┘           └──────┘        └┘ └─┘          └───────┘
txt     └────┘           └──────┘           └─┘          └───────┘
par     └────┘           └──────┘           └─┘          └───────┘
pid       └──┘           └──────┘           └─┘          └───────┘
st     └────────────────────┘└────────────────┘└──────────────────┘└─
599     exact fintype.card_eq.1 (by simp)
id            └─────────────┘
src     └────┘└─────────────┘└─┘   └──┘└─
typ     └────┘└─────────────┘└─┘   └──┘└─
doc     └────┘               └─┘   └──┘└─
txt     └────┘               └─┘   └──┘└─
par     └────┘               └─┘   └──┘└─
pid                         └─┘   └────┘
st   ─────────────────────────────┘└───┘└─
600  
src  
typ  
doc  
txt  
par  
pid  
st   
601  theorem card_le_of_finset {α} (s : finset α) :
id                                      └────┘ 
src                                     └────┘
typ                                     └────┘ 
doc                                     └────┘
602    (s.card : cardinal) ≤ cardinal.mk α :=
id      └───┘   └──────┘   └─────────┘ 
src      └───┘   └──────┘   └─────────┘
typ     └───┘   └──────┘   └─────────┘ 
doc      └───┘   └──────┘    └─────────┘
603  begin
st   └─────
604    rw (_ : (s.card : cardinal) = cardinal.mk (↑s : set α)),
id              └────┘   └──────┘   └─────────┘     └─┘ 
src    └─┘ └──┘ └────┘└─┘└──────┘└┘└─────────┘  └─┘└─┘ └┘
typ    └─┘ └──┘ └────┘└─┘└──────┘└┘└─────────┘ └─┘└─┘└┘
doc    └─┘ └──┘ └────┘└─┘└──────┘└┘ └─────────┘   └─┘    └┘
txt    └─┘ └──┘       └─┘        └┘               └─┘    └┘
par    └─┘ └──┘       └─┘        └┘               └─┘    └┘
pid       └──┘       └─┘        └┘               └─┘    └┘
st   ────────────────────────────────────────────────────────┘└─
605    { exact ⟨function.embedding.subtype _⟩ },
id              └────────────────────────┘
src      └────┘ └────────────────────────┘└──┘
typ      └────┘ └────────────────────────┘└──┘
doc      └────┘                           └──┘
txt      └────┘                           └──┘
par      └────┘                           └──┘
pid                                      └─┘
st   ───┘└───────────────────────────────────┘└┘
606    rw [cardinal.fintype_card, fintype.card_coe]
id         └───────────────────┘  └──────────────┘
src    └──┘└───────────────────┘└┘└──────────────┘└┘
typ    └──┘└───────────────────┘└┘└──────────────┘└┘
doc    └──┘                     └┘                └┘
txt    └──┘                     └┘                └┘
par    └──┘                     └┘                └┘
pid      └┘                     └┘                
st   ──────────────────────────┘└────────────────┘
607  end
st   └─┘
608  
609  @[simp, move_cast] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
id                                                        └─┘      └──────┘     
src                                                       └─┘        └──────┘     
typ                                                       └─┘      └──────┘     
doc    └──┘  └───────┘                                                 └──────┘      
610  by induction n; simp [nat.pow_succ, -_root_.add_comm, power_add, *]
id                        └──────────┘                    └───────┘
src     └────────┘   └────┘└──────────┘└──────────────────┘└───────┘└────
typ     └────────┘  └────┘└──────────┘└──────────────────┘└───────┘└────
doc     └────────┘   └────┘            └──────────────────┘         └────
txt     └────────┘   └────┘            └──────────────────┘         └────
par     └────────┘   └────┘            └──────────────────┘         └────
pid                                 └──────────────────┘         └──┘
st     └─────────────────────────────────────────────────────────────────
611  
src  
typ  
doc  
txt  
par  
pid  
st   
612  @[simp, elim_cast] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
id                                                         └──────┘       
src                                                         └──────┘        
typ                                                        └──────┘       
doc    └──┘  └───────┘                                       └──────┘
613  by rw [← lift_mk_fin, ← lift_mk_fin, lift_le]; exact
id            └─────────┘    └─────────┘  └─────┘
src     └────┘└─────────┘└──┘└─────────┘└┘└─────┘  └────┘
typ     └────┘└─────────┘└──┘└─────────┘└┘└─────┘  └────┘
doc     └────┘           └──┘           └┘         └────┘
txt     └────┘           └──┘           └┘         └────┘
par     └────┘           └──┘           └┘         └────┘
pid       └──┘           └──┘           └┘              
st     └────────────────┘└─────────────┘└───────┘└───────
614  ⟨λ ⟨⟨f, hf⟩⟩, begin
src    └┘  └┘  └──┘     
typ    └┘  └┘  └──┘     
doc    └┘  └┘  └──┘     
txt    └┘  └┘  └──┘     
par    └┘  └┘  └──┘     
pid    └┘  └┘  └──┘     
st   ─────────────┘└─────
615    have : _ = fintype.card _ := finset.card_image_of_injective finset.univ hf,
id               └──────────┘      └────────────────────────────┘ └─────────┘ └┘
src  ─┘└───────┘└──────────┘└────┘└────────────────────────────┘└─────────┘  └─
typ  ─┘└───────┘└──────────┘└────┘└────────────────────────────┘└─────────┘└┘└─
doc  ─┘└───────┘ └──────────┘└────┘                              └─────────┘  └─
txt  ─┘└───────┘             └────┘                                           └─
par  ─┘└───────┘             └────┘                                           └─
pid  ──────────┘             └────┘                                           └─
st   ───────────────────────────────────────────────────────────────────────────┘└─
616    simp at this,
src  ─┘└──────────┘└─
typ  ─┘└──────────┘└─
doc  ─┘└──────────┘└─
txt  ─┘└──────────┘└─
par  ─┘└──────────┘└─
pid  ────────────────
st   ─────────────┘└─
617    rw [← fintype.card_fin n, ← this],
id           └──────────────┘     └──┘
src  ─┘└────┘└──────────────┘ └──┘    └─
typ  ─┘└────┘└──────────────┘└──┘└──┘└─
doc  ─┘└────┘                 └──┘    └─
txt  ─┘└────┘                 └──┘    └─
par  ─┘└────┘                 └──┘    └─
pid  ───────┘                 └──┘    └──
st   ─────────────────────────┘└──────┘└──
618    exact finset.card_le_of_subset (finset.subset_univ _)
id           └──────────────────────┘  └────────────────┘
src  ───────┘└──────────────────────┘ └────────────────┘└───
typ  ───────┘└──────────────────────┘ └────────────────┘└───
doc  ───────┘                                           └───
txt  ───────┘                                           └───
par  ───────┘                                           └───
pid  ───────┘                                           └───
st   ───────────────────────────────────────────────────────┘
619  end,
src  ────┘
typ  ────┘
doc  ────┘
txt  ────┘
par  ────┘
pid  ────┘
st   └─┘└─
620  λ h, ⟨⟨λ i, ⟨i.1, lt_of_lt_of_le i.2 h⟩, λ a b h,
id                     └────────────┘
src   └──┘   └──┘  └──┘└────────────┘ └─┘ └─┘ └───────
typ   └──┘   └──┘  └──┘└────────────┘ └─┘ └─┘ └───────
doc   └──┘   └──┘  └──┘               └─┘ └─┘ └───────
txt   └──┘   └──┘  └──┘               └─┘ └─┘ └───────
par   └──┘   └──┘  └──┘               └─┘ └─┘ └───────
pid   └──┘   └──┘  └──┘               └─┘ └─┘ └───────
st   ──────────────────────────────────────────────────
621    have _, from fin.veq_of_eq h, fin.eq_of_veq this⟩⟩⟩
id                  └───────────┘    └───────────┘
src  ─┘    └───────┘└───────────┘ └┘└───────────┘    └───
typ  ─┘    └───────┘└───────────┘ └┘└───────────┘    └───
doc  ─┘    └───────┘              └┘                 └───
txt  ─┘    └───────┘              └┘                 └───
par  ─┘    └───────┘              └┘                 └───
pid  ─┘    └───────┘              └┘                 └─┘
st   ──────────────────────────────────────────────────────
622  
src  
typ  
doc  
txt  
par  
pid  
st   
623  @[simp, elim_cast] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=
id                                                         └──────┘       
src                                                         └──────┘        
typ                                                        └──────┘       
doc    └──┘  └───────┘                                       └──────┘
624  by simp [lt_iff_le_not_le, -not_le]
id            └──────────────┘
src     └────┘└──────────────┘└──────────
typ     └────┘└──────────────┘└──────────
doc     └────┘                └──────────
txt     └────┘                └──────────
par     └────┘                └──────────
pid                         └────────┘
st     └─────────────────────────────────
625  
src  
typ  
doc  
txt  
par  
pid  
st   
626  @[simp, elim_cast] theorem nat_cast_inj {m n : ℕ} : (m : cardinal) = n ↔ m = n :=
id                                                          └──────┘       
src                                                          └──────┘        
typ                                                         └──────┘       
doc    └──┘  └───────┘                                        └──────┘
627  by simp [le_antisymm_iff]
id            └─────────────┘
src     └────┘└─────────────┘└─
typ     └────┘└─────────────┘└─
doc     └────┘               └─
txt     └────┘               └─
par     └────┘               └─
pid                        
st     └───────────────────────
628  
src  
typ  
doc  
txt  
par  
pid  
st   
629  @[simp, elim_cast] theorem nat_succ (n : ℕ) : succ n = n.succ :=
id                                                └──┘   └───┘
src                                               └──┘     └───┘
typ                                               └──┘   └───┘
doc    └──┘  └───────┘                             └──┘
630  le_antisymm (succ_le.2 $ nat_cast_lt.2 $ nat.lt_succ_self _) (add_one_le_succ _)
id   └─────────┘  └─────┘    └─────────┘    └──────────────┘     └─────────────┘
src  └─────────┘  └─────┘    └─────────┘    └──────────────┘     └─────────────┘
typ  └─────────┘  └─────┘    └─────────┘    └──────────────┘     └─────────────┘
631  
632  @[simp] theorem succ_zero : succ 0 = 1 :=
id                               └──┘   
src                              └──┘   
typ                              └──┘   
doc    └──┘                      └──┘
633  by simpa using nat_succ 0
id                  └──────┘
src     └──────────┘└──────┘└──
typ     └──────────┘└──────┘└──
doc     └──────────┘        └──
txt     └──────────┘        └──
par     └──────────┘        └──
pid          └────┘        └─
st     └───────────────────────
634  
src  
typ  
doc  
txt  
par  
pid  
st   
635  theorem cantor' (a) {b : cardinal} (hb : 1 < b) : a < b ^ a :=
id                            └──────┘                   
src                           └──────┘                     
typ                           └──────┘                   
doc                           └──────┘                       
636  by rw [← succ_le, (by simpa using nat_succ 1 : succ 1 = 2)] at hb;
id            └─────┘                  └──────┘     └──┘   
src     └────┘└─────┘└┘   └──────────┘└──────┘└─┘└┘└──┘└─┘└────────┘
typ     └────┘└─────┘└┘   └──────────┘└──────┘└─┘└┘└──┘└─┘└────────┘
doc     └────┘       └┘   └──────────┘        └─┘└┘└──┘└─┘ └────────┘
txt     └────┘       └┘   └──────────┘        └─┘└┘    └─┘ └────────┘
par     └────┘       └┘   └──────────┘        └─┘└┘    └─┘ └────────┘
pid       └──┘       └┘   └───────────┘        └───┘    └─┘ └──┘└────┘
st     └────────────┘└───┘└──────────────────────┘└───────────┘└───────
637     exact lt_of_lt_of_le (cantor _) (power_le_power_right hb)
id            └────────────┘  └────┘     └──────────────────┘ └┘
src     └────┘└────────────┘ └────┘└──┘ └──────────────────┘  └─
typ     └────┘└────────────┘ └────┘└──┘ └──────────────────┘└┘└─
doc     └────┘                     └──┘                       └─
txt     └────┘                     └──┘                       └─
par     └────┘                     └──┘                       └─
pid                               └──┘                       
st   ─────────────────────────────────────────────────────────────
638  
src  
typ  
doc  
txt  
par  
pid  
st   
639  theorem one_le_iff_pos {c : cardinal} : 1 ≤ c ↔ 0 < c :=
id                               └──────┘            
src                              └──────┘            
typ                              └──────┘            
doc                              └──────┘
640  by rw [← succ_zero, succ_le]
id            └───────┘  └─────┘
src     └────┘└───────┘└┘└─────┘└─
typ     └────┘└───────┘└┘└─────┘└─
doc     └────┘         └┘       └─
txt     └────┘         └┘       └─
par     └────┘         └┘       └─
pid       └──┘         └┘       
st     └──────────────┘└───────┘
641  
src  
typ  
doc  
txt  
par  
pid  
st   
642  theorem one_le_iff_ne_zero {c : cardinal} : 1 ≤ c ↔ c ≠ 0 :=
id                                   └──────┘          
src                                  └──────┘            
typ                                  └──────┘          
doc                                  └──────┘
643  by rw [one_le_iff_pos, pos_iff_ne_zero]
id          └────────────┘  └─────────────┘
src     └──┘└────────────┘└┘└─────────────┘└─
typ     └──┘└────────────┘└┘└─────────────┘└─
doc     └──┘              └┘               └─
txt     └──┘              └┘               └─
par     └──┘              └┘               └─
pid       └┘              └┘               
st     └─────────────────┘└───────────────┘
644  
src  
typ  
doc  
txt  
par  
pid  
st   
645  theorem nat_lt_omega (n : ℕ) : (n : cardinal.{u}) < omega :=
id                                     └──────┘       └───┘
src                                     └──────┘       └───┘
typ                                    └──────┘       └───┘
doc                                      └──────┘        └───┘
646  succ_le.1 $ by rw [nat_succ, ← lift_mk_fin, omega, lift_mk_le.{0 0 u}]; exact
id   └─────┘           └──────┘    └─────────┘  └───┘  └────────┘
src  └─────┘       └──┘└──────┘└──┘└─────────┘└┘└───┘└┘└────────┘└───────┘  └────┘
typ  └─────┘       └──┘└──────┘└──┘└─────────┘└┘└───┘└┘└────────┘└───────┘  └────┘
doc                 └──┘        └──┘           └┘└───┘└┘          └───────┘  └────┘
txt                 └──┘        └──┘           └┘     └┘          └───────┘  └────┘
par                 └──┘        └──┘           └┘     └┘          └───────┘  └────┘
pid                   └┘        └──┘           └┘     └┘          └───────┘       
st                 └───────────┘└─────────────┘└─────┘└──────────────────┘└───────
647  ⟨⟨fin.val, λ a b, fin.eq_of_veq⟩⟩
id     └─────┘         └───────────┘
src    └─────┘└┘ └────┘└───────────┘└──
typ    └─────┘└┘ └────┘└───────────┘└──
doc           └┘ └────┘             └──
txt           └┘ └────┘             └──
par           └┘ └────┘             └──
pid           └┘ └────┘             └┘
st   ──────────────────────────────────
648  
src  
typ  
doc  
txt  
par  
pid  
st   
649  theorem one_lt_omega : 1 < omega :=
id                             └───┘
src                            └───┘
typ                            └───┘
doc                             └───┘
650  by simpa using nat_lt_omega 1
id                  └──────────┘
src     └──────────┘└──────────┘└──
typ     └──────────┘└──────────┘└──
doc     └──────────┘            └──
txt     └──────────┘            └──
par     └──────────┘            └──
pid          └────┘            └─
st     └───────────────────────────
651  
src  
typ  
doc  
txt  
par  
pid  
st   
652  theorem lt_omega {c : cardinal.{u}} : c < omega ↔ ∃ n : ℕ, c = n :=
id                         └──────┘          └───┘          
src                        └──────┘           └───┘          
typ                        └──────┘          └───┘          
doc                        └──────┘            └───┘
653  ⟨λ h, begin
id      
typ     
st         └─────
654    rcases lt_lift_iff.1 h with ⟨c, rfl, h'⟩,
id            └─────────┘   
src    └─────┘└─────────┘└─┘ └────────────────┘
typ    └─────┘└─────────┘└─┘└────────────────┘
doc    └─────┘           └─┘ └────────────────┘
txt    └─────┘           └─┘ └────────────────┘
par    └─────┘           └─┘ └────────────────┘
pid                     └─┘ └────────────────┘
st   ─────────────────────────────────────────┘└─
655    rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩,
id            └──────────────────┘   └┘
src    └─────┘└──────────────────┘└─┘  └──────────────┘
typ    └─────┘└──────────────────┘└─┘└┘└──────────────┘
doc    └─────┘                    └─┘  └──────────────┘
txt    └─────┘                    └─┘  └──────────────┘
par    └─────┘                    └─┘  └──────────────┘
pid                              └─┘  └──────────────┘
st   ─────────────────────────────────────────────────┘└─
656    suffices : finite S,
id                └────┘ 
src    └─────────┘└────┘
typ    └─────────┘└────┘
doc    └─────────┘└────┘
txt    └─────────┘      
par    └─────────┘      
pid    └───────┘└┘      
st   ────────────────────┘└─
657    { cases this, resetI,
id             └──┘
src      └────┘      └────┘
typ      └────┘└──┘  └────┘
doc      └────┘      └────┘
txt      └────┘      └────┘
par      └────┘      └────┘
pid           
st   ───┘└────────┘└─────────
658      existsi fintype.card S,
id               └──────────┘ 
src      └──────┘└──────────┘
typ      └──────┘└──────────┘
doc      └──────┘└──────────┘
txt      └──────┘            
par      └──────┘            
pid                         
st   ─────────────────────────┘└─
659      rw [← lift_nat_cast.{0 u}, lift_inj, fintype_card S] },
id             └───────────┘        └──────┘  └──────────┘ 
src      └────┘└───────────┘└──────┘└──────┘└┘└──────────┘ └┘
typ      └────┘└───────────┘└──────┘└──────┘└┘└──────────┘└┘
doc      └────┘             └──────┘        └┘             └┘
txt      └────┘             └──────┘        └┘             └┘
par      └────┘             └──────┘        └┘             └┘
pid        └──┘             └──────┘        └┘             
st   ────────────────────────────┘└────────┘└──────────────┘└┘
660    by_contra nf,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid             └─┘
st   ─────────────┘└─
661    have P : ∀ (n : ℕ) (IH : ∀ i<n, S), ∃ a : S, ¬ ∃ y h, IH y h = a :=
id                                                               
src    └───────┘ └────┘ └──────┘ └─┘     └───┘   └──┘     └───
typ    └───────┘ └────┘ └──────┘ └─┘     └───┘  └──┘     └───
doc    └───────┘ └────┘ └──────┘ └─┘     └───┘    └──┘       └───
txt    └───────┘ └────┘ └──────┘ └─┘     └───┘    └──┘       └───
par    └───────┘ └────┘ └──────┘ └─┘     └───┘    └──┘       └───
pid    └────┘└─┘ └────┘ └──────┘ └─┘     └───┘    └──┘       └───
st   ──────────────────────────────────────────────────────────────────────
662      λ n IH,
src  ───┘ └──────
typ  ───┘ └──────
doc  ───┘ └──────
txt  ───┘ └──────
par  ───┘ └──────
pid  ───┘ └──────
st   ────────────
663      let g : {i | i < n} → S := λ ⟨i, h⟩, IH i h in
id                                    
src  ───┘   └───┘└──┘   └┘  └──┘ └┘ └┘ └─┘    └───
typ  ───┘   └───┘└──┘   └┘└──┘ └┘└┘└─┘    └───
doc  ───┘   └───┘ └──┘   └┘  └──┘ └┘ └┘ └─┘    └───
txt  ───┘   └───┘ └──┘   └┘  └──┘ └┘ └┘ └─┘    └───
par  ───┘   └───┘ └──┘   └┘  └──┘ └┘ └┘ └─┘    └───
pid  ───┘   └───┘ └──┘   └┘  └──┘ └┘ └┘ └─┘    └───
st   ───────────────────────────────────────────────────
664      classical.not_forall.1 (λ h, nf
id       └──────────────────┘         └┘
src  ───┘└──────────────────┘└─┘  └──┘  
typ  ───┘└──────────────────┘└─┘  └──┘└┘
doc  ───┘                    └─┘  └──┘  
txt  ───┘                    └─┘  └──┘  
par  ───┘                    └─┘  └──┘  
pid  ───┘                    └─┘  └──┘  
st   ────────────────────────────────────
665        ⟨fintype.of_surjective g (λ a, subtype.exists.2 (h a))⟩),
id          └───────────────────┘         └────────────┘
src  ─────┘ └───────────────────┘   └──┘└────────────┘└─┘   └──┘
typ  ─────┘ └───────────────────┘   └──┘└────────────┘└─┘   └──┘
doc  ─────┘ └───────────────────┘   └──┘              └─┘   └──┘
txt  ─────┘                         └──┘              └─┘   └──┘
par  ─────┘                         └──┘              └─┘   └──┘
pid  ─────┘                         └──┘              └─┘   └──┘
st   ─────────────────────────────────────────────────────────────┘└─
666    let F : ℕ → S := nat.lt_wf.fix (λ n IH, classical.some (P n IH)),
id                     └───────────┘          └────────────┘  
src    └──────┘   └──┘└───────────┘  └─────┘└────────────┘     └┘
typ    └──────┘  └──┘└───────────┘  └─────┘└────────────┘    └┘
doc    └──────┘   └──┘               └─────┘                   └┘
txt    └──────┘   └──┘               └─────┘                   └┘
par    └──────┘   └──┘               └─────┘                   └┘
pid    └───┘└─┘   └──┘               └─────┘                   └┘
st   ─────────────────────────────────────────────────────────────────┘└─
667    refine not_le_of_lt h' ⟨⟨F, _⟩⟩,
id            └──────────┘ └┘   
src    └─────┘└──────────┘     └───┘
typ    └─────┘└──────────┘└┘  └───┘
doc    └─────┘                 └───┘
txt    └─────┘                 └───┘
par    └─────┘                 └───┘
pid                           └───┘
st   ────────────────────────────────┘└─
668    suffices : ∀ (n : ℕ) (m < n), F m ≠ F n,
id                                        
src    └─────────┘ └────┘ └─────┘     
typ    └─────────┘ └────┘ └─────┘    
doc    └─────────┘ └────┘ └─────┘      
txt    └─────────┘ └────┘ └─────┘      
par    └─────────┘ └────┘ └─────┘      
pid    └───────┘└┘ └────┘ └─────┘      
st   ────────────────────────────────────────┘└─
669    { refine λ m n, not_imp_not.1 (λ ne, _),
id                     └─────────┘
src      └─────┘ └────┘└─────────┘└─┘  └─────┘
typ      └─────┘ └────┘└─────────┘└─┘  └─────┘
doc      └─────┘ └────┘           └─┘  └─────┘
txt      └─────┘ └────┘           └─┘  └─────┘
par      └─────┘ └────┘           └─┘  └─────┘
pid             └────┘           └─┘  └─────┘
st   ───┘└───────────────────────────────────┘└─
670      rcases lt_trichotomy m n with h|h|h,
id              └───────────┘  
src      └─────┘└───────────┘  └─────────┘
typ      └─────┘└───────────┘└─────────┘
doc      └─────┘               └─────────┘
txt      └─────┘               └─────────┘
par      └─────┘               └─────────┘
pid                           └─────────┘
st   ──────────────────────────────────────┘└─
671      { exact this n m h },
id               └──┘   
src        └────┘       
typ        └────┘└──┘
doc        └────┘       
txt        └────┘       
par        └────┘       
pid                    
st   ─────┘└───────────────┘└┘
672      { contradiction },
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid                     
st   ─────┘└────────────┘└┘
673      { exact (this m n h).symm } },
id                └──┘   
src        └────┘        └─────┘
typ        └────┘ └──┘└─────┘
doc        └────┘        └─────┘
txt        └────┘        └─────┘
par        └────┘        └─────┘
pid                     └───┘└┘
st   ─────────────────────────────┘└──┘
674    intros n m h,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid          └────┘
st   ─────────────┘└─
675    have := classical.some_spec (P n (λ y _, F y)),
id             └─────────────────┘            
src    └──────┘└─────────────────┘     └────┘  └┘
typ    └──────┘└─────────────────┘   └────┘ └┘
doc    └──────┘                        └────┘  └┘
txt    └──────┘                        └────┘  └┘
par    └──────┘                        └────┘  └┘
pid    └───┘└─┘                        └────┘  └┘
st   ───────────────────────────────────────────────┘└─
676    rw [← show F n = classical.some (P n (λ y _, F y)),
id                                                 
src    └────┘                          └────┘  └───
typ    └────┘                         └────┘ └───
doc    └────┘                          └────┘  └───
txt    └────┘                          └────┘  └───
par    └────┘                          └────┘  └───
pid      └──┘                          └────┘  └───
st   ──────────────────────────────────────────────────────
677        from nat.lt_wf.fix_eq (λ n IH, classical.some (P n IH)) n] at this,
id              └──────────────┘          └────────────┘          
src  ──────────┘└──────────────┘  └─────┘└────────────┘     └─┘ └───────┘
typ  ──────────┘└──────────────┘  └─────┘└────────────┘    └─┘└───────┘
doc  ──────────┘                  └─────┘                   └─┘ └───────┘
txt  ──────────┘                  └─────┘                   └─┘ └───────┘
par  ──────────┘                  └─────┘                   └─┘ └───────┘
pid  ──────────┘                  └─────┘                   └─┘ └──────┘
st   ──────────────────────────────────────────────────────────────┘└──────┘└─
678    exact λ e, this ⟨m, h, e⟩,
id                └──┘    
src    └────┘ └──┘      └┘ └┘ 
typ    └────┘ └──┘└──┘ └┘└┘ 
doc    └────┘ └──┘      └┘ └┘ 
txt    └────┘ └──┘      └┘ └┘ 
par    └────┘ └──┘      └┘ └┘ 
pid          └──┘      └┘ └┘ 
st   ──────────────────────────┘└─
679  end, λ ⟨n, e⟩, e.symm ▸ nat_lt_omega _⟩
id                 └───┘  └──────────┘
src                  └───┘  └──────────┘
typ                └───┘  └──────────┘
st   ──┘
680  
681  theorem omega_le {c : cardinal.{u}} : omega ≤ c ↔ ∀ n : ℕ, (n:cardinal) ≤ c :=
id                         └──────┘        └───┘              └──────┘   
src                        └──────┘        └───┘                └──────┘  
typ                        └──────┘        └───┘              └──────┘   
doc                        └──────┘        └───┘                   └──────┘
682  ⟨λ h n, le_trans (le_of_lt (nat_lt_omega _)) h,
id         └──────┘  └──────┘  └──────────┘     
src          └──────┘  └──────┘  └──────────┘
typ        └──────┘  └──────┘  └──────────┘     
683   λ h, le_of_not_lt $ λ hn, begin
id        └──────────┘     └┘
src        └──────────┘
typ       └──────────┘     └┘
st                              └─────
684    rcases lt_omega.1 hn with ⟨n, rfl⟩,
id            └──────┘   └┘
src    └─────┘└──────┘└─┘  └────────────┘
typ    └─────┘└──────┘└─┘└┘└────────────┘
doc    └─────┘        └─┘  └────────────┘
txt    └─────┘        └─┘  └────────────┘
par    └─────┘        └─┘  └────────────┘
pid                  └─┘  └────────────┘
st   ───────────────────────────────────┘└─
685    exact not_le_of_lt (nat.lt_succ_self _) (nat_cast_le.1 (h (n+1)))
id           └──────────┘  └──────────────┘     └─────────┘      
src    └────┘└──────────┘ └──────────────┘└──┘ └─────────┘└─┘    └───┘
typ    └────┘└──────────┘ └──────────────┘└──┘ └─────────┘└─┘  └───┘
doc    └────┘                             └──┘            └─┘     └───┘
txt    └────┘                             └──┘            └─┘     └───┘
par    └────┘                             └──┘            └─┘     └───┘
pid                                      └──┘            └─┘     └──┘
st   ───────────────────────────────────────────────────────────────────┘
686  end⟩
st   └─┘
687  
688  theorem lt_omega_iff_fintype {α : Type u} : mk α < omega ↔ nonempty (fintype α) :=
id                                               └┘   └───┘  └──────┘  └─────┘ 
src                                              └┘    └───┘  └──────┘  └─────┘
typ                                              └┘   └───┘  └──────┘  └─────┘ 
doc                                              └┘     └───┘             └─────┘
689  lt_omega.trans ⟨λ ⟨n, e⟩, begin
id   └──────┘└────┘    
src  └──────┘└────┘
typ  └──────┘└────┘    
st                             └─────
690    rw [← lift_mk_fin n] at e,
id           └─────────┘ 
src    └────┘└─────────┘ └────┘
typ    └────┘└─────────┘└────┘
doc    └────┘            └────┘
txt    └────┘            └────┘
par    └────┘            └────┘
pid      └──┘            └───┘
st   ────────────────────┘└───┘└─
691    cases quotient.exact e with f,
id           └────────────┘ 
src    └────┘└────────────┘ └─────┘
typ    └────┘└────────────┘└─────┘
doc    └────┘               └─────┘
txt    └────┘               └─────┘
par    └────┘               └─────┘
pid                        └─────┘
st   ──────────────────────────────┘└─
692    exact ⟨fintype.of_equiv _ f.symm⟩
id            └──────────────┘   └────┘
src    └────┘ └──────────────┘└─┘└────┘└┘
typ    └────┘ └──────────────┘└─┘└────┘└┘
doc    └────┘ └──────────────┘└─┘      └┘
txt    └────┘                 └─┘      └┘
par    └────┘                 └─┘      └┘
pid                          └─┘      
st   ───────────────────────────────────┘
693  end, λ ⟨_⟩, by exactI ⟨_, fintype_card _⟩⟩
id                            └──────────┘
src                 └─────┘ └─┘└──────────┘└─┘
typ                └─────┘ └─┘└──────────┘└─┘
doc                 └─────┘ └─┘            └─┘
txt                 └─────┘ └─┘            └─┘
par                 └─────┘ └─┘            └─┘
pid                        └─┘            └─┘
st   └─┘           └─────────────────────────┘
694  
695  theorem lt_omega_iff_finite {α} {S : set α} : mk S < omega ↔ finite S :=
id                                        └─┘     └┘   └───┘  └────┘ 
src                                       └─┘      └┘    └───┘  └────┘
typ                                       └─┘     └┘   └───┘  └────┘ 
doc                                                └┘     └───┘   └────┘
696  lt_omega_iff_fintype
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
697  
698  instance can_lift_cardinal_nat : can_lift cardinal ℕ :=
id                                    └──────┘ └──────┘ 
src                                   └──────┘ └──────┘ 
typ                                   └──────┘ └──────┘ 
doc                                   └──────┘ └──────┘
699  ⟨ coe, λ x, x < omega, λ x hx, let ⟨n, hn⟩ := lt_omega.mp hx in ⟨n, hn.symm⟩⟩
id     └─┘        └───┘     └┘  └─┘    └┘     └──────┘└─┘ └┘          └───┘
src    └─┘          └───┘                         └──────┘└─┘             └───┘
typ    └─┘        └───┘     └┘  └─┘    └┘     └──────┘└─┘ └┘          └───┘
doc                  └───┘
700  
701  theorem add_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a + b < omega :=
id                               └──────┘          └───┘          └───┘        └───┘
src                              └──────┘           └───┘           └───┘          └───┘
typ                              └──────┘          └───┘          └───┘        └───┘
doc                              └──────┘            └───┘            └───┘            └───┘
702  match a, b, lt_omega.1 ha, lt_omega.1 hb with
id             └──────┘  └┘  └──────┘  └┘
src              └──────┘      └──────┘
typ            └──────┘  └┘  └──────┘  └┘
703  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat.cast_add]; apply nat_lt_omega
id                         └─┘              └──────────┘         └──────────┘
src                        └─┘        └────┘└──────────┘  └────┘└──────────┘
typ                        └─┘        └────┘└──────────┘  └────┘└──────────┘
doc                                   └────┘              └────┘            
txt                                   └────┘              └────┘            
par                                   └────┘              └────┘            
pid                                     └──┘                               
st                                   └─────────────────┘└───────────────────┘
704  end
705  
706  lemma add_lt_omega_iff {a b : cardinal} : a + b < omega ↔ a < omega ∧ b < omega :=
id                                 └──────┘        └───┘    └───┘    └───┘
src                                └──────┘          └───┘     └───┘     └───┘
typ                                └──────┘        └───┘    └───┘    └───┘
doc                                └──────┘            └───┘       └───┘       └───┘
707  ⟨λ h, ⟨lt_of_le_of_lt (le_add_right _ _) h, lt_of_le_of_lt (le_add_left _ _) h⟩,
id         └────────────┘  └──────────┘        └────────────┘  └─────────┘      
src         └────────────┘  └──────────┘         └────────────┘  └─────────┘
typ        └────────────┘  └──────────┘        └────────────┘  └─────────┘      
708    λ⟨h1, h2⟩, add_lt_omega h1 h2⟩
id      └┘  └┘   └──────────┘
src               └──────────┘
typ     └┘  └┘   └──────────┘
709  
710  theorem mul_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a * b < omega :=
id                               └──────┘          └───┘          └───┘        └───┘
src                              └──────┘           └───┘           └───┘          └───┘
typ                              └──────┘          └───┘          └───┘        └───┘
doc                              └──────┘            └───┘            └───┘            └───┘
711  match a, b, lt_omega.1 ha, lt_omega.1 hb with
id             └──────┘  └┘  └──────┘  └┘
src              └──────┘      └──────┘
typ            └──────┘  └┘  └──────┘  └┘
712  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat.cast_mul]; apply nat_lt_omega
id                         └─┘              └──────────┘         └──────────┘
src                        └─┘        └────┘└──────────┘  └────┘└──────────┘
typ                        └─┘        └────┘└──────────┘  └────┘└──────────┘
doc                                   └────┘              └────┘            
txt                                   └────┘              └────┘            
par                                   └────┘              └────┘            
pid                                     └──┘                               
st                                   └─────────────────┘└───────────────────┘
713  end
714  
715  lemma mul_lt_omega_iff {a b : cardinal} : a * b < omega ↔ a = 0 ∨ b = 0 ∨ a < omega ∧ b < omega :=
id                                 └──────┘        └───┘              └───┘    └───┘
src                                └──────┘          └───┘                 └───┘     └───┘
typ                                └──────┘        └───┘              └───┘    └───┘
doc                                └──────┘            └───┘                       └───┘       └───┘
716  begin
st   └─────
717    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
718    { intro h, by_cases ha : a = 0, { left, exact ha },
id                                                 └┘
src      └─────┘  └───────┘  └─┘ └┘    └──┘  └────┘  
typ      └─────┘  └───────┘  └─┘└┘    └──┘  └────┘└┘
doc      └─────┘  └───────┘  └─┘  └┘    └──┘  └────┘  
txt      └─────┘  └───────┘  └─┘  └┘    └──┘  └────┘  
par      └─────┘  └───────┘  └─┘  └┘    └──┘  └────┘  
pid           └┘            └─┘                   
st   ───┘└─────┘└───────────────────┘└──┘└──┘└─────────┘└┘
719      right, by_cases hb : b = 0, { left, exact hb },
id                                                └┘
src      └───┘  └───────┘  └─┘  └┘    └──┘  └────┘  
typ      └───┘  └───────┘  └─┘ └┘    └──┘  └────┘└┘
doc      └───┘  └───────┘  └─┘  └┘    └──┘  └────┘  
txt      └───┘  └───────┘  └─┘  └┘    └──┘  └────┘  
par      └───┘  └───────┘  └─┘  └┘    └──┘  └────┘  
pid                       └─┘                   
st   ────────┘└───────────────────┘└──┘└──┘└─────────┘└┘
720      right, rw [← ne, ← one_le_iff_ne_zero] at ha hb, split,
id                    └┘    └────────────────┘
src      └───┘  └────┘└┘└──┘└────────────────┘└────────┘  └───┘
typ      └───┘  └────┘└┘└──┘└────────────────┘└────────┘  └───┘
doc      └───┘  └────┘  └──┘                  └────────┘  └───┘
txt      └───┘  └────┘  └──┘                  └────────┘  └───┘
par      └───┘  └────┘  └──┘                  └────────┘  └───┘
pid               └──┘  └──┘                  └───────┘
st   ────────┘└────────┘└────────────────────┘└───────┘└─────┘└─
721      { rw [← mul_one a], refine lt_of_le_of_lt (mul_le_mul (le_refl a) hb) h },
id               └─────┘           └────────────┘  └────────┘  └─────┘   └┘  
src        └────┘└─────┘   └─────┘└────────────┘ └────────┘ └─────┘ └┘  └┘ 
typ        └────┘└─────┘  └─────┘└────────────┘ └────────┘ └─────┘└┘└┘└┘
doc        └────┘          └─────┘                                  └┘  └┘ 
txt        └────┘          └─────┘                                  └┘  └┘ 
par        └────┘          └─────┘                                  └┘  └┘ 
pid          └──┘                                                  └┘  └┘ 
st   ─────┘└─────────────┘└─────────────────────────────────────────────────────┘└┘
722      { rw [← _root_.one_mul b], refine lt_of_le_of_lt (mul_le_mul ha (le_refl b)) h }},
id               └────────────┘           └────────────┘  └────────┘ └┘  └─────┘    
src        └────┘└────────────┘   └─────┘└────────────┘ └────────┘   └─────┘ └─┘ 
typ        └────┘└────────────┘  └─────┘└────────────┘ └────────┘└┘ └─────┘└─┘
doc        └────┘                 └─────┘                                    └─┘ 
txt        └────┘                 └─────┘                                    └─┘ 
par        └────┘                 └─────┘                                    └─┘ 
pid          └──┘                                                           └─┘ 
st   ───────────────────────────┘└─────────────────────────────────────────────────────┘└─┘
723    rintro (rfl|rfl|⟨ha,hb⟩); simp only [*, mul_lt_omega, omega_pos, _root_.zero_mul, mul_zero]
id                                             └──────────┘  └───────┘  └─────────────┘  └──────┘
src    └──────────────────────┘  └────────────┘└──────────┘└┘└───────┘└┘└─────────────┘└┘└──────┘└┘
typ    └──────────────────────┘  └────────────┘└──────────┘└┘└───────┘└┘└─────────────┘└┘└──────┘└┘
doc    └──────────────────────┘  └────────────┘            └┘         └┘               └┘        └┘
txt    └──────────────────────┘  └────────────┘            └┘         └┘               └┘        └┘
par    └──────────────────────┘  └────────────┘            └┘         └┘               └┘        └┘
pid          └────────────────┘      └──┘└───┘            └┘         └┘               └┘        
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘
724  end
st   └─┘
725  
726  lemma mul_lt_omega_iff_of_ne_zero {a b : cardinal} (ha : a ≠ 0) (hb : b ≠ 0) :
id                                            └──────┘                    
src                                           └──────┘                      
typ                                           └──────┘                    
doc                                           └──────┘
727    a * b < omega ↔ a < omega ∧ b < omega :=
id         └───┘    └───┘    └───┘
src          └───┘     └───┘     └───┘
typ        └───┘    └───┘    └───┘
doc            └───┘       └───┘       └───┘
728  by simp [mul_lt_omega_iff, ha, hb]
id            └──────────────┘  └┘  └┘
src     └────┘└──────────────┘└┘  └┘  └─
typ     └────┘└──────────────┘└┘└┘└┘└┘└─
doc     └────┘                └┘  └┘  └─
txt     └────┘                └┘  └┘  └─
par     └────┘                └┘  └┘  └─
pid                         └┘  └┘  
st     └────────────────────────────────
729  
src  
typ  
doc  
txt  
par  
pid  
st   
730  theorem power_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a ^ b < omega :=
id                                 └──────┘          └───┘          └───┘        └───┘
src                                └──────┘           └───┘           └───┘          └───┘
typ                                └──────┘          └───┘          └───┘        └───┘
doc                                └──────┘            └───┘            └───┘           └───┘
731  match a, b, lt_omega.1 ha, lt_omega.1 hb with
id             └──────┘  └┘  └──────┘  └┘
src              └──────┘      └──────┘
typ            └──────┘  └┘  └──────┘  └┘
732  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat_cast_pow]; apply nat_lt_omega
id                         └─┘              └──────────┘         └──────────┘
src                        └─┘        └────┘└──────────┘  └────┘└──────────┘
typ                        └─┘        └────┘└──────────┘  └────┘└──────────┘
doc                                   └────┘              └────┘            
txt                                   └────┘              └────┘            
par                                   └────┘              └────┘            
pid                                     └──┘                               
st                                   └─────────────────┘└───────────────────┘
733  end
734  
735  lemma eq_one_iff_subsingleton_and_nonempty {α : Type*} :
736    mk α = 1 ↔ (subsingleton α ∧ nonempty α) :=
id     └┘       └──────────┘   └──────┘ 
src    └┘        └──────────┘    └──────┘
typ    └┘       └──────────┘   └──────┘ 
doc    └┘
737  calc mk α = 1 ↔ mk α ≤ 1 ∧ ¬mk α < 1 : eq_iff_le_not_lt
id        └┘       └┘      └┘       └──────────────┘
src       └┘        └┘       └┘        └──────────────┘
typ       └┘       └┘      └┘       └──────────────┘
doc       └┘         └┘          └┘
738            ... ↔ subsingleton α ∧ nonempty α :
id                   └──────────┘   └──────┘ 
src                  └──────────┘    └──────┘
typ                  └──────────┘   └──────┘ 
739  begin
st   └─────
740    apply and_congr le_one_iff_subsingleton,
id           └───────┘ └─────────────────────┘
src    └────┘└───────┘└─────────────────────┘
typ    └────┘└───────┘└─────────────────────┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                  
st   ────────────────────────────────────────┘└─
741    push_neg,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
st   ─────────┘└─
742    rw [one_le_iff_ne_zero, ne_zero_iff_nonempty]
id         └────────────────┘  └──────────────────┘
src    └──┘└────────────────┘└┘└──────────────────┘└┘
typ    └──┘└────────────────┘└┘└──────────────────┘└┘
doc    └──┘                  └┘                    └┘
txt    └──┘                  └┘                    └┘
par    └──┘                  └┘                    └┘
pid      └┘                  └┘                    
st   ───────────────────────┘└────────────────────┘
743  end
st   └─┘
744  
745  theorem infinite_iff {α : Type u} : infinite α ↔ omega ≤ mk α :=
id                                       └──────┘   └───┘  └┘ 
src                                      └──────┘    └───┘  └┘
typ                                      └──────┘   └───┘  └┘ 
doc                                                   └───┘   └┘
746  by rw [←not_lt, lt_omega_iff_fintype, not_nonempty_fintype]
id           └────┘  └──────────────────┘  └──────────────────┘
src     └───┘└────┘└┘└──────────────────┘└┘└──────────────────┘└─
typ     └───┘└────┘└┘└──────────────────┘└┘└──────────────────┘└─
doc     └───┘      └┘                    └┘                    └─
txt     └───┘      └┘                    └┘                    └─
par     └───┘      └┘                    └┘                    └─
pid       └─┘      └┘                    └┘                    
st     └──────────┘└────────────────────┘└────────────────────┘
747  
src  
typ  
doc  
txt  
par  
pid  
st   
748  lemma countable_iff (s : set α) : countable s ↔ mk s ≤ omega :=
id                            └─┘     └───────┘   └┘   └───┘
src                           └─┘      └───────┘    └┘    └───┘
typ                           └─┘     └───────┘   └┘   └───┘
doc                                    └───────┘     └┘     └───┘
749  begin
st   └─────
750    rw [countable_iff_exists_injective], split,
id         └────────────────────────────┘
src    └──┘└────────────────────────────┘  └───┘
typ    └──┘└────────────────────────────┘  └───┘
doc    └──┘                                └───┘
txt    └──┘                                └───┘
par    └──┘                                └───┘
pid      └┘                              
st   ───────────────────────────────────┘└──────┘└─
751    rintro ⟨f, hf⟩, exact ⟨embedding.trans ⟨f, hf⟩ equiv.ulift.symm.to_embedding⟩,
id                            └─────────────┘    └┘  └───────────────────────────┘
src    └────────────┘  └────┘ └─────────────┘  └┘  └┘└───────────────────────────┘
typ    └────────────┘  └────┘ └─────────────┘ └┘└┘└┘└───────────────────────────┘
doc    └────────────┘  └────┘                  └┘  └┘                             
txt    └────────────┘  └────┘                  └┘  └┘                             
par    └────────────┘  └────┘                  └┘  └┘                             
pid          └──────┘                         └┘  └┘                             
st   ───────────────┘└─────────────────────────────────────────────────────────────┘└─
752    rintro ⟨f'⟩, cases embedding.trans f' equiv.ulift.to_embedding with f hf, exact ⟨f, hf⟩
id                        └─────────────┘ └┘ └──────────────────────┘                     └┘
src    └─────────┘  └────┘└─────────────┘  └──────────────────────┘└────────┘  └────┘  └┘  └┘
typ    └─────────┘  └────┘└─────────────┘└┘└──────────────────────┘└────────┘  └────┘ └┘└┘└┘
doc    └─────────┘  └────┘                                         └────────┘  └────┘  └┘  └┘
txt    └─────────┘  └────┘                                         └────────┘  └────┘  └┘  └┘
par    └─────────┘  └────┘                                         └────────┘  └────┘  └┘  └┘
pid          └───┘                                                └────────┘         └┘  
st   ────────────┘└───────────────────────────────────────────────────────────┘└──────────────┘
753  end
st   └─┘
754  
755  lemma denumerable_iff {α : Type u} : nonempty (denumerable α) ↔ mk α = omega :=
id                                        └──────┘  └─────────┘    └┘   └───┘
src                                       └──────┘  └─────────┘     └┘    └───┘
typ                                       └──────┘  └─────────┘    └┘   └───┘
doc                                                 └─────────┘      └┘     └───┘
756  ⟨λ⟨h⟩, quotient.sound $ by exactI ⟨ (denumerable.eqv α).trans equiv.ulift.symm ⟩,
id         └────────────┘                └─────────────┘         └──────────────┘
src         └────────────┘      └─────┘  └─────────────┘ └──────┘└──────────────┘└┘
typ        └────────────┘      └─────┘  └─────────────┘└──────┘└──────────────┘└┘
doc                             └─────┘                  └──────┘                └┘
txt                             └─────┘                  └──────┘                └┘
par                             └─────┘                  └──────┘                └┘
pid                                                     └──────┘                └┘
st                             └────────────────────────────────────────────────────┘
757   λ h, by { cases quotient.exact h with f, exact ⟨denumerable.mk' $ f.trans equiv.ulift⟩ }⟩
id                   └────────────┘                 └─────────────┘   └─────┘ └─────────┘
src             └────┘└────────────┘ └─────┘  └────┘ └─────────────┘ └─────┘└─────────┘└┘
typ            └────┘└────────────┘└─────┘  └────┘ └─────────────┘ └─────┘└─────────┘└┘
doc             └────┘               └─────┘  └────┘                                   └┘
txt             └────┘               └─────┘  └────┘                                   └┘
par             └────┘               └─────┘  └────┘                                   └┘
pid                                 └─────┘                                          
st           └──────────────────────────────┘└──────────────────────────────────────────────┘└┘
758  
759  lemma mk_int : mk ℤ = omega :=
id                  └┘   └───┘
src                 └┘   └───┘
typ                 └┘   └───┘
doc                 └┘     └───┘
760  denumerable_iff.mp ⟨by apply_instance⟩
id   └─────────────┘└─┘
src  └─────────────┘└─┘     └────────────┘
typ  └─────────────┘└─┘     └────────────┘
doc                         └────────────┘
txt                         └────────────┘
par                         └────────────┘
st                         └─────────────┘
761  
762  lemma mk_pnat : mk ℕ+ = omega :=
id                   └┘ └┘  └───┘
src                  └┘ └┘  └───┘
typ                  └┘ └┘  └───┘
doc                  └┘ └┘   └───┘
763  denumerable_iff.mp ⟨by apply_instance⟩
id   └─────────────┘└─┘
src  └─────────────┘└─┘     └────────────┘
typ  └─────────────┘└─┘     └────────────┘
doc                         └────────────┘
txt                         └────────────┘
par                         └────────────┘
st                         └─────────────┘
764  
765  lemma two_le_iff : (2 : cardinal) ≤ mk α ↔ ∃x y : α, x ≠ y :=
id                           └──────┘   └┘            
src                          └──────┘   └┘              
typ                          └──────┘   └┘            
doc                          └──────┘    └┘
766  begin
st   └─────
767    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
768    { rintro ⟨f⟩, refine ⟨f $ sum.inl ⟨⟩, f $ sum.inr ⟨⟩, _⟩, intro h, cases f.2 h },
id                               └─────┘       └─────┘                          
src      └────────┘  └─────┘   └─────┘└─┘  └─────┘└───┘  └─────┘  └────┘ └─┘ 
typ      └────────┘  └─────┘   └─────┘└─┘ └─────┘└───┘  └─────┘  └────┘└─┘
doc      └────────┘  └─────┘           └─┘          └───┘  └─────┘  └────┘ └─┘ 
txt      └────────┘  └─────┘           └─┘          └───┘  └─────┘  └────┘ └─┘ 
par      └────────┘  └─────┘           └─┘          └───┘  └─────┘  └────┘ └─┘ 
pid            └──┘                   └─┘          └───┘       └┘        └─┘ 
st   ───┘└────────┘└──────────────────────────────────────────┘└───────┘└────────────┘└┘
769    { rintro ⟨x, y, h⟩, by_contra h',
src      └──────────────┘  └──────────┘
typ      └──────────────┘  └──────────┘
doc      └──────────────┘  └──────────┘
txt      └──────────────┘  └──────────┘
par      └──────────────┘  └──────────┘
pid            └────────┘           └─┘
st   ───────────────────┘└────────────┘└─
770      rw [not_le, ←nat.cast_two, ←nat_succ, lt_succ, nat.cast_one, le_one_iff_subsingleton] at h',
id           └────┘   └──────────┘   └──────┘  └─────┘  └──────────┘  └─────────────────────┘
src      └──┘└────┘└─┘└──────────┘└─┘└──────┘└┘└─────┘└┘└──────────┘└┘└─────────────────────┘└─────┘
typ      └──┘└────┘└─┘└──────────┘└─┘└──────┘└┘└─────┘└┘└──────────┘└┘└─────────────────────┘└─────┘
doc      └──┘      └─┘            └─┘        └┘       └┘            └┘                       └─────┘
txt      └──┘      └─┘            └─┘        └┘       └┘            └┘                       └─────┘
par      └──┘      └─┘            └─┘        └┘       └┘            └┘                       └─────┘
pid        └┘      └─┘            └─┘        └┘       └┘            └┘                       └────┘
st   ─────────────┘└─────────────┘└─────────┘└───────┘└────────────┘└───────────────────────┘└────┘└─
771      apply h, exactI subsingleton.elim _ _ }
id                       └───────────────┘
src      └────┘   └─────┘└───────────────┘└───┘
typ      └────┘   └─────┘└───────────────┘└───┘
doc      └────┘   └─────┘                 └───┘
txt      └────┘   └─────┘                 └───┘
par      └────┘   └─────┘                 └───┘
pid                                     └──┘
st   ──────────┘└─────────────────────────────┘└─
772  end
st   ──┘
773  
774  lemma two_le_iff' (x : α) : (2 : cardinal) ≤ mk α ↔ ∃y : α, x ≠ y :=
id                                   └──────┘   └┘          
src                                   └──────┘   └┘            
typ                                  └──────┘   └┘          
doc                                   └──────┘    └┘
775  begin
st   └─────
776    rw [two_le_iff],
id         └────────┘
src    └──┘└────────┘
typ    └──┘└────────┘
doc    └──┘          
txt    └──┘          
par    └──┘          
pid      └┘          
st   ───────────────┘└──
777    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
778    { rintro ⟨y, z, h⟩, refine classical.by_cases (λ(h' : x = y), _) (λ h', ⟨y, h'⟩),
id                                └────────────────┘                          
src      └──────────────┘  └─────┘└────────────────┘  └────┘  └────┘  └───┘  └┘  └┘
typ      └──────────────┘  └─────┘└────────────────┘  └────┘ └────┘  └───┘ └┘  └┘
doc      └──────────────┘  └─────┘                    └────┘   └────┘  └───┘  └┘  └┘
txt      └──────────────┘  └─────┘                    └────┘   └────┘  └───┘  └┘  └┘
par      └──────────────┘  └─────┘                    └────┘   └────┘  └───┘  └┘  └┘
pid            └────────┘                            └────┘   └────┘  └───┘  └┘  └┘
st   ───┘└──────────────┘└────────────────────────────────────────────────────────────┘└─
779      rw [←h'] at h, exact ⟨z, h⟩ },
id            └┘                 
src      └───┘  └────┘  └────┘  └┘ └┘
typ      └───┘└┘└────┘  └────┘ └┘└┘
doc      └───┘  └────┘  └────┘  └┘ └┘
txt      └───┘  └────┘  └────┘  └┘ └┘
par      └───┘  └────┘  └────┘  └┘ └┘
pid        └─┘  └───┘         └┘ 
st   ──────────┘└───┘└─────────────┘└┘
780    { rintro ⟨y, h⟩, exact ⟨x, y, h⟩ }
id                                 
src      └───────────┘  └────┘  └┘ └┘ └┘
typ      └───────────┘  └────┘ └┘└┘└┘
doc      └───────────┘  └────┘  └┘ └┘ └┘
txt      └───────────┘  └────┘  └┘ └┘ └┘
par      └───────────┘  └────┘  └┘ └┘ └┘
pid            └─────┘         └┘ └┘ 
st   ────────────────┘└────────────────┘└─
781  end
st   ──┘
782  
783  /-- König's theorem -/
784  theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
id                                     └──────┘                   └─┘   └──┘ 
src                                     └──────┘                        └─┘    └──┘
typ                                    └──────┘                   └─┘   └──┘ 
doc                                     └──────┘                         └─┘     └──┘
785  lt_of_not_ge $ λ ⟨F⟩, begin
id   └──────────┘     
src  └──────────┘
typ  └──────────┘     
st                         └─────
786    have : inhabited (Π (i : ι), (g i).out),
id            └───────┘             
src    └─────┘└───────┘  └────┘     └────┘
typ    └─────┘└───────┘  └────┘   └────┘
doc    └─────┘           └────┘     └────┘
txt    └─────┘           └────┘     └────┘
par    └─────┘           └────┘     └────┘
pid    └───┘└┘           └────┘     └────┘
st   ────────────────────────────────────────┘└─
787    { refine ⟨λ i, classical.choice $ ne_zero_iff_nonempty.1 _⟩,
id                    └──────────────┘   └──────────────────┘
src      └─────┘  └──┘└──────────────┘ └──────────────────┘└───┘
typ      └─────┘  └──┘└──────────────┘ └──────────────────┘└───┘
doc      └─────┘  └──┘                                     └───┘
txt      └─────┘  └──┘                                     └───┘
par      └─────┘  └──┘                                     └───┘
pid              └──┘                                     └───┘
st   ───┘└───────────────────────────────────────────────────────┘└─
788      rw mk_out,
id          └────┘
src      └─┘└────┘
typ      └─┘└────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────┘└─
789      exact ne_of_gt (lt_of_le_of_lt (zero_le _) (H i)) }, resetI,
id             └──────┘  └────────────┘  └─────┘      
src      └────┘└──────┘ └────────────┘ └─────┘└──┘   └─┘   └────┘
typ      └────┘└──────┘ └────────────┘ └─────┘└──┘ └─┘   └────┘
doc      └────┘                               └──┘   └─┘   └────┘
txt      └────┘                               └──┘   └─┘   └────┘
par      └────┘                               └──┘   └─┘   └────┘
pid                                          └──┘   └┘
st   ─────────────────────────────────────────────────────┘└┘└────────
790    let G := inv_fun F,
id              └─────┘ 
src    └───────┘└─────┘
typ    └───────┘└─────┘
doc    └───────┘└─────┘
txt    └───────┘       
par    └───────┘       
pid    └───┘└─┘       
st   ───────────────────┘└─
791    have sG : surjective G := inv_fun_surjective F.2,
id               └────────┘     └────────────────┘ 
src    └────────┘└────────┘ └──┘└────────────────┘ └┘
typ    └────────┘└────────┘└──┘└────────────────┘└┘
doc    └────────┘           └──┘                   └┘
txt    └────────┘           └──┘                   └┘
par    └────────┘           └──┘                   └┘
pid    └─────┘└─┘           └──┘                   └┘
st   ─────────────────────────────────────────────────┘└─
792    choose C hc using show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b,
id                                                   
src    └────────────────┘     └┘ └┘ └┘    └┘ └┘  └─
typ    └────────────────┘     └┘ └┘ └┘   └┘ └┘  └─
doc    └────────────────┘     └┘  └┘  └┘    └┘ └┘   └─
txt    └────────────────┘     └┘  └┘  └┘    └┘ └┘   └─
par    └────────────────┘     └┘  └┘  └┘    └┘ └┘   └─
pid          └┘└─┘└─────┘     └┘  └┘  └┘    └┘ └┘   └─
st   ────────────────────────────────────────────────────────
793    { assume i,
src  ───┘└──────┘└─
typ  ───┘└──────┘└─
doc  ───┘└──────┘└─
txt  ───┘└──────┘└─
par  ───┘└──────┘└─
pid  ──────────────
st   ──┘└───────┘└─
794      simp only [- not_exists, not_exists.symm, classical.not_forall.symm],
src  ───┘└───────────────────────┘               └┘                         └─
typ  ───┘└───────────────────────┘└─────────────┘└┘└───────────────────────┘└─
doc  ───┘└───────────────────────┘               └┘                         └─
txt  ───┘└───────────────────────┘               └┘                         └─
par  ───┘└───────────────────────┘               └┘                         └─
pid  ────────────────────────────┘               └┘                         └──
st   ───────────────────────────────────────────────────────────────────────┘└─
795      refine λ h, not_le_of_lt (H i) _,
id                   └──────────┘   
src  ───┘└─────┘ └──┘└──────────┘   └─┘└─
typ  ───┘└─────┘ └──┘└──────────┘ └─┘└─
doc  ───┘└─────┘ └──┘               └─┘└─
txt  ───┘└─────┘ └──┘               └─┘└─
par  ───┘└─────┘ └──┘               └─┘└─
pid  ──────────┘ └──┘               └────
st   ───────────────────────────────────┘└─
796      rw [← mk_out (f i), ← mk_out (g i)],
id             └────┘        └────┘   
src  ───┘└────┘└────┘   └───┘└────┘   └┘└─
typ  ───┘└────┘└────┘ └───┘└────┘ └┘└─
doc  ───┘└────┘         └───┘         └┘└─
txt  ───┘└────┘         └───┘         └┘└─
par  ───┘└────┘         └───┘         └┘└─
pid  ─────────┘         └───┘         └───
st   ─────────────────────┘└──────────────┘└──
797      exact ⟨embedding.of_surjective h⟩ },
id              └─────────────────────┘ 
src  ───┘└────┘ └─────────────────────┘ └┘
typ  ───┘└────┘ └─────────────────────┘└┘
doc  ───┘└────┘                         └┘
txt  ───┘└────┘                         └┘
par  ───┘└────┘                         └┘
pid  ─────────┘                         └─┘
st   ─────────────────────────────────────┘└┘
798    exact (let ⟨⟨i, a⟩, h⟩ := sG C in hc i a (congr_fun h _))
id                            └┘     └┘      └───────┘
src    └────┘       └┘ └─┘ └───┘   └──┘     └───────┘ └───┘
typ    └────┘      └┘└─┘└───┘└┘└──┘└┘   └───────┘ └───┘
doc    └────┘       └┘ └─┘ └───┘   └──┘               └───┘
txt    └────┘       └┘ └─┘ └───┘   └──┘               └───┘
par    └────┘       └┘ └─┘ └───┘   └──┘               └───┘
pid                └┘ └─┘ └───┘   └──┘               └──┘
st   ───────────────────────────────────────────────────────────┘
799  end
st   └─┘
800  
801  @[simp] theorem mk_empty : mk empty = 0 :=
id                              └┘ └───┘ 
src                             └┘ └───┘ 
typ                             └┘ └───┘ 
doc    └──┘                     └┘
802  fintype_card empty
id   └──────────┘ └───┘
src  └──────────┘ └───┘
typ  └──────────┘ └───┘
803  
804  @[simp] theorem mk_pempty : mk pempty = 0 :=
id                               └┘ └────┘ 
src                              └┘ └────┘ 
typ                              └┘ └────┘ 
doc    └──┘                      └┘ └────┘
805  fintype_card pempty
id   └──────────┘ └────┘
src  └──────────┘ └────┘
typ  └──────────┘ └────┘
doc               └────┘
806  
807  @[simp] theorem mk_plift_of_false {p : Prop} (h : ¬ p) : mk (plift p) = 0 :=
id                                                          └┘  └───┘   
src                                                          └┘  └───┘    
typ                                                         └┘  └───┘   
doc    └──┘                                                   └┘  └───┘
808  quotient.sound ⟨equiv.plift.trans $ equiv.equiv_pempty h⟩
id   └────────────┘  └─────────┘└────┘   └────────────────┘ 
src  └────────────┘  └─────────┘└────┘   └────────────────┘
typ  └────────────┘  └─────────┘└────┘   └────────────────┘ 
809  
810  @[simp] theorem mk_unit : mk unit = 1 :=
id                             └┘ └──┘ 
src                            └┘ └──┘ 
typ                            └┘ └──┘ 
doc    └──┘                    └┘ └──┘
811  (fintype_card unit).trans nat.cast_one
id    └──────────┘ └──┘ └───┘  └──────────┘
src   └──────────┘ └──┘ └───┘  └──────────┘
typ   └──────────┘ └──┘ └───┘  └──────────┘
doc                └──┘
812  
813  @[simp] theorem mk_punit : mk punit = 1 :=
id                              └┘ └───┘ 
src                             └┘ └───┘ 
typ                             └┘ └───┘ 
doc    └──┘                     └┘
814  (fintype_card punit).trans nat.cast_one
id    └──────────┘ └───┘ └───┘  └──────────┘
src   └──────────┘ └───┘ └───┘  └──────────┘
typ   └──────────┘ └───┘ └───┘  └──────────┘
815  
816  @[simp] theorem mk_singleton {α : Type u} (x : α) : mk ({x} : set α) = 1 :=
id                                                      └┘      └─┘   
src                                                      └┘       └─┘    
typ                                                     └┘      └─┘   
doc    └──┘                                              └┘
817  quotient.sound ⟨equiv.set.singleton x⟩
id   └────────────┘  └─────────────────┘ 
src  └────────────┘  └─────────────────┘
typ  └────────────┘  └─────────────────┘ 
818  
819  @[simp] theorem mk_plift_of_true {p : Prop} (h : p) : mk (plift p) = 1 :=
id                                                        └┘  └───┘   
src                                                        └┘  └───┘    
typ                                                       └┘  └───┘   
doc    └──┘                                                └┘  └───┘
820  quotient.sound ⟨equiv.plift.trans $ equiv.prop_equiv_punit h⟩
id   └────────────┘  └─────────┘└────┘   └────────────────────┘ 
src  └────────────┘  └─────────┘└────┘   └────────────────────┘
typ  └────────────┘  └─────────┘└────┘   └────────────────────┘ 
821  
822  @[simp] theorem mk_bool : mk bool = 2 :=
id                             └┘ └──┘ 
src                            └┘ └──┘ 
typ                            └┘ └──┘ 
doc    └──┘                    └┘
823  quotient.sound ⟨equiv.bool_equiv_punit_sum_punit⟩
id   └────────────┘  └──────────────────────────────┘
src  └────────────┘  └──────────────────────────────┘
typ  └────────────┘  └──────────────────────────────┘
824  
825  @[simp] theorem mk_Prop : mk Prop = 2 :=
id                             └┘      
src                            └┘      
typ                            └┘      
doc    └──┘                    └┘
826  (quotient.sound ⟨equiv.Prop_equiv_bool⟩ : mk Prop = mk bool).trans mk_bool
id    └────────────┘  └───────────────────┘    └┘       └┘ └──┘ └───┘  └─────┘
src   └────────────┘  └───────────────────┘    └┘       └┘ └──┘ └───┘  └─────┘
typ   └────────────┘  └───────────────────┘    └┘       └┘ └──┘ └───┘  └─────┘
doc                                            └┘        └┘
827  
828  @[simp] theorem mk_option {α : Type u} : mk (option α) = mk α + 1 :=
id                                            └┘  └────┘    └┘  
src                                           └┘  └────┘     └┘   
typ                                           └┘  └────┘    └┘  
doc    └──┘                                   └┘              └┘
829  quotient.sound ⟨equiv.option_equiv_sum_punit α⟩
id   └────────────┘  └──────────────────────────┘ 
src  └────────────┘  └──────────────────────────┘
typ  └────────────┘  └──────────────────────────┘ 
830  
831  theorem mk_list_eq_sum_pow (α : Type u) : mk (list α) = sum (λ n : ℕ, (mk α)^(n:cardinal.{u})) :=
id                                             └┘  └──┘    └─┘           └┘    └──────┘
src                                            └┘  └──┘     └─┘           └┘      └──────┘
typ                                            └┘  └──┘    └─┘           └┘    └──────┘
doc                                            └┘            └─┘            └┘      └──────┘
832  calc  mk (list α)
id         └┘  └──┘ 
src        └┘  └──┘
typ        └┘  └──┘ 
doc        └┘
833      = mk (Σ n, vector α n) : quotient.sound ⟨(equiv.sigma_preimage_equiv list.length).symm⟩
id         └┘    └────┘      └────────────┘   └────────────────────────┘ └─────────┘ └──┘
src        └┘     └────┘        └────────────┘   └────────────────────────┘ └─────────┘ └──┘
typ        └┘    └────┘      └────────────┘   └────────────────────────┘ └─────────┘ └──┘
doc        └┘
834  ... = mk (Σ n, fin n → α) : quotient.sound ⟨equiv.sigma_congr_right $ λ n,
id         └┘    └─┘        └────────────┘  └─────────────────────┘     
src        └┘     └─┘          └────────────┘  └─────────────────────┘
typ        └┘    └─┘        └────────────┘  └─────────────────────┘     
doc        └┘
835    ⟨vector.nth, vector.of_fn, vector.of_fn_nth, λ f, funext $ vector.nth_of_fn f⟩⟩
id      └────────┘  └──────────┘  └──────────────┘      └────┘   └──────────────┘ 
src     └────────┘  └──────────┘  └──────────────┘       └────┘   └──────────────┘
typ     └────────┘  └──────────┘  └──────────────┘      └────┘   └──────────────┘ 
836  ... = mk (Σ n : ℕ, ulift.{u} (fin n) → α) : quotient.sound ⟨equiv.sigma_congr_right $ λ n,
id         └┘        └───┘      └─┘         └────────────┘  └─────────────────────┘     
src        └┘        └───┘      └─┘           └────────────┘  └─────────────────────┘
typ        └┘        └───┘      └─┘         └────────────┘  └─────────────────────┘     
doc        └┘           └───┘
837    equiv.arrow_congr equiv.ulift.symm (equiv.refl α)⟩
id     └───────────────┘ └─────────┘└───┘  └────────┘ 
src    └───────────────┘ └─────────┘└───┘  └────────┘
typ    └───────────────┘ └─────────┘└───┘  └────────┘ 
838  ... = sum (λ n : ℕ, (mk α)^(n:cardinal.{u})) : by simp only [(lift_mk_fin _).symm, lift_mk, power_def, sum_mk]
id         └─┘           └┘    └──────┘                        └─────────┘          └─────┘  └───────┘  └────┘
src        └─┘           └┘      └──────┘            └─────────┘ └─────────┘└────────┘└─────┘└┘└───────┘└┘└────┘└─
typ        └─┘           └┘    └──────┘            └─────────┘ └─────────┘└────────┘└─────┘└┘└───────┘└┘└────┘└─
doc        └─┘            └┘      └──────┘            └─────────┘            └────────┘       └┘         └┘      └─
txt                                                    └─────────┘            └────────┘       └┘         └┘      └─
par                                                    └─────────┘            └────────┘       └┘         └┘      └─
pid                                                        └──┘└┘            └────────┘       └┘         └┘      
st                                                    └─────────────────────────────────────────────────────────────
839  
src  
typ  
doc  
txt  
par  
pid  
st   
840  theorem mk_quot_le {α : Type u} {r : α → α → Prop} : mk (quot r) ≤ mk α :=
id                                                      └┘  └──┘    └┘ 
src                                                       └┘           └┘
typ                                                     └┘  └──┘    └┘ 
doc                                                       └┘            └┘
841  mk_le_of_surjective quot.exists_rep
id   └─────────────────┘ └─────────────┘
src  └─────────────────┘ └─────────────┘
typ  └─────────────────┘ └─────────────┘
842  
843  theorem mk_quotient_le {α : Type u} {s : setoid α} : mk (quotient s) ≤ mk α :=
id                                            └────┘     └┘  └──────┘    └┘ 
src                                           └────┘      └┘  └──────┘     └┘
typ                                           └────┘     └┘  └──────┘    └┘ 
doc                                                       └┘                └┘
844  mk_quot_le
id   └────────┘
src  └────────┘
typ  └────────┘
845  
846  theorem mk_subtype_le {α : Type u} (p : α → Prop) : mk (subtype p) ≤ mk α :=
id                                                      └┘  └─────┘    └┘ 
src                                                      └┘  └─────┘     └┘
typ                                                     └┘  └─────┘    └┘ 
doc                                                      └┘               └┘
847  ⟨embedding.subtype p⟩
id    └───────────────┘ 
src   └───────────────┘
typ   └───────────────┘ 
848  
849  theorem mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x⦄, p x → q x) :
id                                                                                
typ                                                                               
850    mk (subtype p) ≤ mk (subtype q) :=
id     └┘  └─────┘    └┘  └─────┘ 
src    └┘  └─────┘     └┘  └─────┘
typ    └┘  └─────┘    └┘  └─────┘ 
doc    └┘               └┘
851  ⟨embedding.subtype_map (embedding.refl α) h⟩
id    └───────────────────┘  └────────────┘   
src   └───────────────────┘  └────────────┘
typ   └───────────────────┘  └────────────┘   
852  
853  @[simp] theorem mk_emptyc (α : Type u) : mk (∅ : set α) = 0 :=
id                                            └┘     └─┘   
src                                           └┘     └─┘    
typ                                           └┘     └─┘   
doc    └──┘                                   └┘
854  quotient.sound ⟨equiv.set.pempty α⟩
id   └────────────┘  └──────────────┘ 
src  └────────────┘  └──────────────┘
typ  └────────────┘  └──────────────┘ 
855  
856  theorem mk_univ {α : Type u} : mk (@univ α) = mk α :=
id                                  └┘   └──┘    └┘ 
src                                 └┘   └──┘     └┘
typ                                 └┘   └──┘    └┘ 
doc                                 └┘             └┘
857  quotient.sound ⟨equiv.set.univ α⟩
id   └────────────┘  └────────────┘ 
src  └────────────┘  └────────────┘
typ  └────────────┘  └────────────┘ 
858  
859  theorem mk_image_le {α β : Type u} {f : α → β} {s : set α} : mk (f '' s) ≤ mk s :=
id                                                     └─┘     └┘   └┘    └┘ 
src                                                      └─┘      └┘    └┘     └┘
typ                                                    └─┘     └┘   └┘    └┘ 
doc                                                               └┘            └┘
860  mk_le_of_surjective surjective_onto_image
id   └─────────────────┘ └───────────────────┘
src  └─────────────────┘ └───────────────────┘
typ  └─────────────────┘ └───────────────────┘
861  
862  theorem mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : set α} :
id                                                                     └─┘ 
src                                                                      └─┘
typ                                                                    └─┘ 
863    lift.{v u} (mk (f '' s)) ≤ lift.{u v} (mk s) :=
id     └──┘        └┘   └┘     └──┘        └┘ 
src    └──┘        └┘    └┘      └──┘        └┘
typ    └──┘        └┘   └┘     └──┘        └┘ 
doc    └──┘        └┘             └──┘        └┘
864  lift_mk_le.{v u 0}.mpr ⟨embedding.of_surjective surjective_onto_image⟩
id   └────────┘        └─┘   └─────────────────────┘ └───────────────────┘
src  └────────┘        └─┘   └─────────────────────┘ └───────────────────┘
typ  └────────┘        └─┘   └─────────────────────┘ └───────────────────┘
865  
866  theorem mk_range_le {α β : Type u} {f : α → β} : mk (range f) ≤ mk α :=
id                                                  └┘  └───┘    └┘ 
src                                                   └┘  └───┘     └┘
typ                                                 └┘  └───┘    └┘ 
doc                                                   └┘  └───┘      └┘
867  mk_le_of_surjective surjective_onto_range
id   └─────────────────┘ └───────────────────┘
src  └─────────────────┘ └───────────────────┘
typ  └─────────────────┘ └───────────────────┘
868  
869  lemma mk_range_eq (f : α → β) (h : injective f) : mk (range f) = mk α :=
id                                    └───────┘     └┘  └───┘    └┘ 
src                                     └───────┘      └┘  └───┘     └┘
typ                                   └───────┘     └┘  └───┘    └┘ 
doc                                                    └┘  └───┘      └┘
870  quotient.sound ⟨(equiv.set.range f h).symm⟩
id   └────────────┘   └─────────────┘   └──┘
src  └────────────┘   └─────────────┘     └──┘
typ  └────────────┘   └─────────────┘   └──┘
871  
872  lemma mk_range_eq_of_inj {α : Type u} {β : Type v} {f : α → β} (hf : injective f) :
id                                                                      └───────┘ 
src                                                                       └───────┘
typ                                                                     └───────┘ 
873    lift.{v u} (mk (range f)) = lift.{u v} (mk α) :=
id     └──┘        └┘  └───┘     └──┘        └┘ 
src    └──┘        └┘  └───┘      └──┘        └┘
typ    └──┘        └┘  └───┘     └──┘        └┘ 
doc    └──┘        └┘  └───┘       └──┘        └┘
874  begin
st   └─────
875    have := (@lift_mk_eq.{v u max u v} (range f) α).2 ⟨(equiv.set.range f hf).symm⟩,
id               └────────┘                └───┘          └─────────────┘  └┘
src    └──────┘  └────────┘└─────────────┘ └───┘ └┘ └──┘  └─────────────┘   └─────┘
typ    └──────┘  └────────┘└─────────────┘ └───┘ └┘└──┘  └─────────────┘└┘└─────┘
doc    └──────┘            └─────────────┘ └───┘ └┘ └──┘                    └─────┘
txt    └──────┘            └─────────────┘       └┘ └──┘                    └─────┘
par    └──────┘            └─────────────┘       └┘ └──┘                    └─────┘
pid    └───┘└─┘            └─────────────┘       └┘ └──┘                    └─────┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
876    simp only [lift_umax.{u v}, lift_umax.{v u}] at this,
id                └───────┘        └───────┘
src    └─────────┘└───────┘└──────┘└───────┘└─────────────┘
typ    └─────────┘└───────┘└──────┘└───────┘└─────────────┘
doc    └─────────┘         └──────┘         └─────────────┘
txt    └─────────┘         └──────┘         └─────────────┘
par    └─────────┘         └──────┘         └─────────────┘
pid        └──┘└┘         └──────┘         └─────┘└─────┘
st   ─────────────────────────────────────────────────────┘└─
877    exact this
id           └──┘
src    └────┘    
typ    └────┘└──┘
doc    └────┘    
txt    └────┘    
par    └────┘    
pid             
st   ────────────┘
878  end
st   └─┘
879  
880  lemma mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : injective f) :
id                                                                    └───────┘ 
src                                                                     └───────┘
typ                                                                   └───────┘ 
881    lift.{v (max u w)} (# (range f)) = lift.{u (max v w)} (# α) :=
id     └──┘                  └───┘     └──┘                 
src    └──┘                  └───┘      └──┘                
typ    └──┘                  └───┘     └──┘                 
doc    └──┘                  └───┘       └──┘                
882  lift_mk_eq.mpr ⟨(equiv.set.range f hf).symm⟩
id   └────────┘└──┘   └─────────────┘  └┘ └──┘
src  └────────┘└──┘   └─────────────┘      └──┘
typ  └────────┘└──┘   └─────────────┘  └┘ └──┘
883  
884  theorem mk_image_eq {α β : Type u} {f : α → β} {s : set α} (hf : injective f) :
id                                                     └─┘         └───────┘ 
src                                                      └─┘          └───────┘
typ                                                    └─┘         └───────┘ 
885    mk (f '' s) = mk s :=
id     └┘   └┘    └┘ 
src    └┘    └┘     └┘
typ    └┘   └┘    └┘ 
doc    └┘            └┘
886  quotient.sound ⟨(equiv.set.image f s hf).symm⟩
id   └────────────┘   └─────────────┘   └┘ └──┘
src  └────────────┘   └─────────────┘        └──┘
typ  └────────────┘   └─────────────┘   └┘ └──┘
887  
888  theorem mk_Union_le_sum_mk {α ι : Type u} {f : ι → set α} : mk (⋃ i, f i) ≤ sum (λ i, mk (f i)) :=
id                                                     └─┘     └┘        └─┘      └┘   
src                                                     └─┘      └┘           └─┘       └┘
typ                                                    └─┘     └┘        └─┘      └┘   
doc                                                              └┘            └─┘       └┘
889  calc mk (⋃ i, f i) ≤ mk (Σ i, f i) : mk_le_of_surjective (set.surjective_sigma_to_Union f)
id        └┘         └┘         └─────────────────┘  └───────────────────────────┘ 
src       └┘            └┘            └─────────────────┘  └───────────────────────────┘
typ       └┘         └┘         └─────────────────┘  └───────────────────────────┘ 
doc       └┘            └┘
890    ... = sum (λ i, mk (f i)) : (sum_mk _).symm
id           └─┘      └┘         └────┘   └──┘
src          └─┘       └┘           └────┘   └──┘
typ          └─┘      └┘         └────┘   └──┘
doc          └─┘       └┘
891  
892  theorem mk_Union_eq_sum_mk {α ι : Type u} {f : ι → set α} (h : ∀i j, i ≠ j → disjoint (f i) (f j)) :
id                                                     └─┘                 └──────┘       
src                                                     └─┘                      └──────┘
typ                                                    └─┘                 └──────┘       
doc                                                                               └──────┘
893    mk (⋃ i, f i) = sum (λ i, mk (f i)) :=
id     └┘        └─┘      └┘   
src    └┘           └─┘       └┘
typ    └┘        └─┘      └┘   
doc    └┘            └─┘       └┘
894  calc mk (⋃ i, f i) = mk (Σi, f i) : quot.sound ⟨set.Union_eq_sigma_of_disjoint h⟩
id        └┘         └┘        └────────┘  └────────────────────────────┘ 
src       └┘            └┘           └────────┘  └────────────────────────────┘
typ       └┘         └┘        └────────┘  └────────────────────────────┘ 
doc       └┘            └┘
895    ... = sum (λi, mk (f i)) : (sum_mk _).symm
id           └─┘     └┘         └────┘   └──┘
src          └─┘      └┘           └────┘   └──┘
typ          └─┘     └┘         └────┘   └──┘
doc          └─┘      └┘
896  
897  lemma mk_Union_le {α ι : Type u} (f : ι → set α) :
id                                            └─┘ 
src                                            └─┘
typ                                           └─┘ 
898    mk (⋃ i, f i) ≤ mk ι * cardinal.sup.{u u} (λ i, mk (f i)) :=
id     └┘        └┘   └──────────┘            └┘   
src    └┘           └┘    └──────────┘             └┘
typ    └┘        └┘   └──────────┘            └┘   
doc    └┘            └┘     └──────────┘             └┘
899  le_trans mk_Union_le_sum_mk (sum_le_sup _)
id   └──────┘ └────────────────┘  └────────┘
src  └──────┘ └────────────────┘  └────────┘
typ  └──────┘ └────────────────┘  └────────┘
900  
901  lemma mk_sUnion_le {α : Type u} (A : set (set α)) :
id                                        └─┘  └─┘ 
src                                       └─┘  └─┘
typ                                       └─┘  └─┘ 
902    mk (⋃₀ A) ≤ mk A * cardinal.sup.{u u} (λ s : A, mk s) :=
id     └┘  └┘    └┘   └──────────┘                └┘ 
src    └┘  └┘     └┘    └──────────┘                 └┘
typ    └┘  └┘    └┘   └──────────┘                └┘ 
doc    └┘          └┘     └──────────┘                 └┘
903  by { rw [sUnion_eq_Union], apply mk_Union_le }
id            └─────────────┘         └─────────┘
src       └──┘└─────────────┘  └────┘└─────────┘
typ       └──┘└─────────────┘  └────┘└─────────┘
doc       └──┘                 └────┘           
txt       └──┘                 └────┘           
par       └──┘                 └────┘           
pid         └┘                                 
st     └────────────────────┘└───────────────────┘└┘
904  
905  lemma mk_bUnion_le {ι α : Type u} (A : ι → set α) (s : set ι) :
id                                             └─┘        └─┘ 
src                                             └─┘         └─┘
typ                                            └─┘        └─┘ 
906    mk (⋃(x ∈ s), A x) ≤ mk s * cardinal.sup.{u u} (λ x : s, mk (A x.1)) :=
id     └┘            └┘   └──────────┘                └┘   
src    └┘                └┘    └──────────┘                 └┘     
typ    └┘            └┘   └──────────┘                └┘   
doc    └┘                 └┘     └──────────┘                 └┘
907  by { rw [bUnion_eq_Union], apply mk_Union_le }
id            └─────────────┘         └─────────┘
src       └──┘└─────────────┘  └────┘└─────────┘
typ       └──┘└─────────────┘  └────┘└─────────┘
doc       └──┘                 └────┘           
txt       └──┘                 └────┘           
par       └──┘                 └────┘           
pid         └┘                                 
st     └────────────────────┘└───────────────────┘└┘
908  
909  @[simp] lemma finset_card {α : Type u} {s : finset α} : ↑(finset.card s) = mk (↑s : set α) :=
id                                               └────┘      └─────────┘    └┘     └─┘ 
src                                              └────┘       └─────────┘     └┘      └─┘
typ                                              └────┘      └─────────┘    └┘     └─┘ 
doc    └──┘                                      └────┘        └─────────┘      └┘
910  by rw [fintype_card, nat_cast_inj, fintype.card_coe]
id          └──────────┘  └──────────┘  └──────────────┘
src     └──┘└──────────┘└┘└──────────┘└┘└──────────────┘└─
typ     └──┘└──────────┘└┘└──────────┘└┘└──────────────┘└─
doc     └──┘            └┘            └┘                └─
txt     └──┘            └┘            └┘                └─
par     └──┘            └┘            └┘                └─
pid       └┘            └┘            └┘                
st     └───────────────┘└────────────┘└────────────────┘
911  
src  
typ  
doc  
txt  
par  
pid  
st   
912  lemma finset_card_lt_omega (s : finset α) : mk (↑s : set α) < omega :=
id                                   └────┘     └┘     └─┘    └───┘
src                                  └────┘      └┘      └─┘     └───┘
typ                                  └────┘     └┘     └─┘    └───┘
doc                                  └────┘      └┘                └───┘
913  by { rw [lt_omega_iff_fintype], exact ⟨finset.subtype.fintype s⟩ }
id            └──────────────────┘          └────────────────────┘ 
src       └──┘└──────────────────┘  └────┘ └────────────────────┘ └┘
typ       └──┘└──────────────────┘  └────┘ └────────────────────┘└┘
doc       └──┘                      └────┘                        └┘
txt       └──┘                      └────┘                        └┘
par       └──┘                      └────┘                        └┘
pid         └┘                                                   
st     └─────────────────────────┘└──────────────────────────────────┘└┘
914  
915  theorem mk_union_add_mk_inter {α : Type u} {S T : set α} : mk (S ∪ T : set α) + mk (S ∩ T : set α) = mk S + mk T :=
id                                                     └─┘     └┘       └─┘    └┘       └─┘    └┘   └┘ 
src                                                    └─┘      └┘         └─┘     └┘         └─┘     └┘    └┘
typ                                                    └─┘     └┘       └─┘    └┘       └─┘    └┘   └┘ 
doc                                                             └┘                   └┘                   └┘     └┘
916  quot.sound ⟨equiv.set.union_sum_inter S T⟩
id   └────────┘  └───────────────────────┘  
src  └────────┘  └───────────────────────┘
typ  └────────┘  └───────────────────────┘  
917  
918  theorem mk_union_of_disjoint {α : Type u} {S T : set α} (H : disjoint S T) : mk (S ∪ T : set α) = mk S + mk T :=
id                                                    └─┘        └──────┘      └┘       └─┘    └┘   └┘ 
src                                                   └─┘         └──────┘        └┘         └─┘     └┘    └┘
typ                                                   └─┘        └──────┘      └┘       └─┘    └┘   └┘ 
doc                                                               └──────┘        └┘                   └┘     └┘
919  quot.sound ⟨equiv.set.union (disjoint_iff.1 H)⟩
id   └────────┘  └─────────────┘  └──────────┘  
src  └────────┘  └─────────────┘  └──────────┘
typ  └────────┘  └─────────────┘  └──────────┘  
920  
921  lemma mk_sum_compl {α} (s : set α) : #s + #(-s : set α) = #α :=
id                               └─┘           └─┘    
src                              └─┘              └─┘     
typ                              └─┘           └─┘    
doc                                                          
922  quotient.sound ⟨equiv.set.sum_compl s⟩
id   └────────────┘  └─────────────────┘ 
src  └────────────┘  └─────────────────┘
typ  └────────────┘  └─────────────────┘ 
923  
924  lemma mk_le_mk_of_subset {α} {s t : set α} (h : s ⊆ t) : mk s ≤ mk t :=
id                                       └─┘              └┘   └┘ 
src                                      └─┘                 └┘    └┘
typ                                      └─┘              └┘   └┘ 
doc                                                           └┘     └┘
925  ⟨ set.embedding_of_subset h ⟩
id     └─────────────────────┘ 
src    └─────────────────────┘
typ    └─────────────────────┘ 
doc    └─────────────────────┘
926  
927  lemma mk_subtype_mono {p q : α → Prop} (h : ∀x, p x → q x) : mk {x // p x} ≤ mk {x // q x} :=
id                                                          └┘         └┘      
src                                                               └┘            └┘ 
typ                                                         └┘         └┘      
doc                                                               └┘              └┘
928  ⟨embedding_of_subset h⟩
id    └─────────────────┘ 
src   └─────────────────┘
typ   └─────────────────┘ 
doc   └─────────────────┘
929  
930  lemma mk_set_le (s : set α) : mk s ≤ mk α :=
id                        └─┘     └┘   └┘ 
src                       └─┘      └┘    └┘
typ                       └─┘     └┘   └┘ 
doc                                └┘     └┘
931  mk_subtype_le s
id   └───────────┘ 
src  └───────────┘
typ  └───────────┘ 
932  
933  lemma mk_image_eq_lift {α : Type u} {β : Type v} (f : α → β) (s : set α) (h : injective f) :
id                                                                   └─┘        └───────┘ 
src                                                                    └─┘         └───────┘
typ                                                                  └─┘        └───────┘ 
934    lift.{v u} (mk (f '' s)) = lift.{u v} (mk s) :=
id     └──┘        └┘   └┘     └──┘        └┘ 
src    └──┘        └┘    └┘      └──┘        └┘
typ    └──┘        └┘   └┘     └──┘        └┘ 
doc    └──┘        └┘             └──┘        └┘
935  lift_mk_eq.{v u 0}.mpr ⟨(equiv.set.image f s h).symm⟩
id   └────────┘        └─┘    └─────────────┘    └──┘
src  └────────┘        └─┘    └─────────────┘       └──┘
typ  └────────┘        └─┘    └─────────────┘    └──┘
936  
937  lemma mk_image_eq_of_inj_on_lift {α : Type u} {β : Type v} (f : α → β) (s : set α)
id                                                                             └─┘ 
src                                                                              └─┘
typ                                                                            └─┘ 
938    (h : inj_on f s) : lift.{v u} (mk (f '' s)) = lift.{u v} (mk s) :=
id          └────┘      └──┘        └┘   └┘     └──┘        └┘ 
src         └────┘        └──┘        └┘    └┘      └──┘        └┘
typ         └────┘      └──┘        └┘   └┘     └──┘        └┘ 
doc         └────┘        └──┘        └┘             └──┘        └┘
939  lift_mk_eq.{v u 0}.mpr ⟨(equiv.set.image_of_inj_on f s h).symm⟩
id   └────────┘        └─┘    └───────────────────────┘    └──┘
src  └────────┘        └─┘    └───────────────────────┘       └──┘
typ  └────────┘        └─┘    └───────────────────────┘    └──┘
940  
941  lemma mk_image_eq_of_inj_on {α β : Type u} (f : α → β) (s : set α) (h : inj_on f s) :
id                                                             └─┘        └────┘  
src                                                              └─┘         └────┘
typ                                                            └─┘        └────┘  
doc                                                                          └────┘
942    mk (f '' s) = mk s :=
id     └┘   └┘    └┘ 
src    └┘    └┘     └┘
typ    └┘   └┘    └┘ 
doc    └┘            └┘
943  quotient.sound ⟨(equiv.set.image_of_inj_on f s h).symm⟩
id   └────────────┘   └───────────────────────┘    └──┘
src  └────────────┘   └───────────────────────┘       └──┘
typ  └────────────┘   └───────────────────────┘    └──┘
944  
945  lemma mk_subtype_of_equiv {α β : Type u} (p : α → Prop) (e : α ≃ β) :
id                                                                 
src                                                                 
typ                                                                
doc                                                                 
946    mk {a : α // p a} = mk {b : β // p (e.symm b)} :=
id     └┘             └┘           └───┘ 
src    └┘                └┘              └───┘
typ    └┘             └┘           └───┘ 
doc    └┘                  └┘
947  quotient.sound ⟨equiv.subtype_equiv_of_subtype' e⟩
id   └────────────┘  └─────────────────────────────┘ 
src  └────────────┘  └─────────────────────────────┘
typ  └────────────┘  └─────────────────────────────┘ 
948  
949  lemma mk_sep (s : set α) (t : α → Prop) : mk ({ x ∈ s | t x } : set α) = mk { x : s | t x.1 } :=
id                     └─┘                   └┘                └─┘    └┘          
src                    └─┘                     └┘                   └─┘     └┘             
typ                    └─┘                   └┘                └─┘    └┘          
doc                                            └┘                             └┘
950  quotient.sound ⟨equiv.set.sep s t⟩
id   └────────────┘  └───────────┘  
src  └────────────┘  └───────────┘
typ  └────────────┘  └───────────┘  
951  
952  lemma mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : set β)
id                                                                                └─┘ 
src                                                                                 └─┘
typ                                                                               └─┘ 
953    (h : injective f) : lift.{u v} (mk (f ⁻¹' s)) ≤ lift.{v u} (mk s) :=
id          └───────┘     └──┘        └┘   └─┘     └──┘        └┘ 
src         └───────┘      └──┘        └┘    └─┘      └──┘        └┘
typ         └───────┘     └──┘        └┘   └─┘     └──┘        └┘ 
doc                        └──┘        └┘    └─┘       └──┘        └┘
954  begin
st   └─────
955    rw lift_mk_le.{u v 0}, use subtype.coind (λ x, f x.1) (λ x, x.2),
id        └────────┘              └───────────┘       
src    └─┘└────────┘└──────┘  └──┘└───────────┘  └──┘  └──┘  └──┘ └─┘
typ    └─┘└────────┘└──────┘  └──┘└───────────┘  └──┘ └──┘  └──┘ └─┘
doc    └─┘          └──────┘  └──┘└───────────┘  └──┘  └──┘  └──┘ └─┘
txt    └─┘          └──────┘  └──┘               └──┘  └──┘  └──┘ └─┘
par    └─┘          └──────┘  └──┘               └──┘  └──┘  └──┘ └─┘
pid                └──────┘                    └──┘  └──┘  └──┘ └─┘
st   ──────────────────────┘└─────────────────────────────────────────┘└─
956    apply subtype.coind_injective, exact injective_comp h subtype.val_injective
id           └─────────────────────┘        └────────────┘  └───────────────────┘
src    └────┘└─────────────────────┘  └────┘└────────────┘ └───────────────────┘
typ    └────┘└─────────────────────┘  └────┘└────────────┘└───────────────────┘
doc    └────┘                         └────┘                                    
txt    └────┘                         └────┘                                    
par    └────┘                         └────┘                                    
pid                                                                           
st   ──────────────────────────────┘└─────────────────────────────────────────────┘
957  end
st   └─┘
958  
959  lemma mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : set β)
id                                                                                   └─┘ 
src                                                                                    └─┘
typ                                                                                  └─┘ 
960    (h : s ⊆ range f) : lift.{v u} (mk s) ≤ lift.{u v} (mk (f ⁻¹' s)) :=
id            └───┘     └──┘        └┘    └──┘        └┘   └─┘ 
src            └───┘      └──┘        └┘     └──┘        └┘    └─┘
typ           └───┘     └──┘        └┘    └──┘        └┘   └─┘ 
doc             └───┘      └──┘        └┘      └──┘        └┘    └─┘
961  begin
st   └─────
962    rw lift_mk_le.{v u 0},
id        └────────┘
src    └─┘└────────┘└──────┘
typ    └─┘└────────┘└──────┘
doc    └─┘          └──────┘
txt    └─┘          └──────┘
par    └─┘          └──────┘
pid                └──────┘
st   ──────────────────────┘└─
963    refine ⟨⟨_, _⟩⟩,
src    └─────┘  └────┘
typ    └─────┘  └────┘
doc    └─────┘  └────┘
txt    └─────┘  └────┘
par    └─────┘  └────┘
pid            └────┘
st   ────────────────┘└─
964    { rintro ⟨y, hy⟩, rcases classical.subtype_of_exists (h hy) with ⟨x, rfl⟩, exact ⟨x, hy⟩ },
id                              └─────────────────────────┘   └┘                          └┘
src      └────────────┘  └─────┘└─────────────────────────┘    └─────────────┘  └────┘  └┘  └┘
typ      └────────────┘  └─────┘└─────────────────────────┘ └┘└─────────────┘  └────┘ └┘└┘└┘
doc      └────────────┘  └─────┘└─────────────────────────┘    └─────────────┘  └────┘  └┘  └┘
txt      └────────────┘  └─────┘                               └─────────────┘  └────┘  └┘  └┘
par      └────────────┘  └─────┘                               └─────────────┘  └────┘  └┘  └┘
pid            └──────┘                                       └─────────────┘         └┘  
st   ───┘└────────────┘└───────────────────────────────────────────────────────┘└──────────────┘└┘
965    rintro ⟨y, hy⟩ ⟨y', hy'⟩, dsimp,
src    └──────────────────────┘  └───┘
typ    └──────────────────────┘  └───┘
doc    └──────────────────────┘  └───┘
txt    └──────────────────────┘  └───┘
par    └──────────────────────┘  └───┘
pid          └────────────────┘
st   ─────────────────────────┘└─────┘└─
966    rcases classical.subtype_of_exists (h hy) with ⟨x, rfl⟩,
id            └─────────────────────────┘   └┘
src    └─────┘└─────────────────────────┘    └─────────────┘
typ    └─────┘└─────────────────────────┘ └┘└─────────────┘
doc    └─────┘└─────────────────────────┘    └─────────────┘
txt    └─────┘                               └─────────────┘
par    └─────┘                               └─────────────┘
pid                                         └─────────────┘
st   ────────────────────────────────────────────────────────┘└─
967    rcases classical.subtype_of_exists (h hy') with ⟨x', rfl⟩,
id            └─────────────────────────┘   └─┘
src    └─────┘└─────────────────────────┘     └──────────────┘
typ    └─────┘└─────────────────────────┘ └─┘└──────────────┘
doc    └─────┘└─────────────────────────┘     └──────────────┘
txt    └─────┘                                └──────────────┘
par    └─────┘                                └──────────────┘
pid                                          └──────────────┘
st   ──────────────────────────────────────────────────────────┘└─
968    simp, intro hxx', rw hxx'
id                          └──┘
src    └──┘  └────────┘  └─┘    
typ    └──┘  └────────┘  └─┘└──┘
doc    └──┘  └────────┘  └─┘    
txt    └──┘  └────────┘  └─┘    
par    └──┘  └────────┘  └─┘    
pid               └───┘        
st   ─────┘└──────────┘└────────┘
969  end
st   └─┘
970  
971  lemma mk_preimage_of_injective_of_subset_range_lift {β : Type v} (f : α → β) (s : set β)
id                                                                                   └─┘ 
src                                                                                    └─┘
typ                                                                                  └─┘ 
972    (h : injective f) (h2 : s ⊆ range f) : lift.{u v} (mk (f ⁻¹' s)) = lift.{v u} (mk s) :=
id          └───────┘           └───┘     └──┘        └┘   └─┘     └──┘        └┘ 
src         └───────┘             └───┘      └──┘        └┘    └─┘      └──┘        └┘
typ         └───────┘           └───┘     └──┘        └┘   └─┘     └──┘        └┘ 
doc                                └───┘      └──┘        └┘    └─┘       └──┘        └┘
973  le_antisymm (mk_preimage_of_injective_lift f s h) (mk_preimage_of_subset_range_lift f s h2)
id   └─────────┘  └───────────────────────────┘      └──────────────────────────────┘   └┘
src  └─────────┘  └───────────────────────────┘         └──────────────────────────────┘
typ  └─────────┘  └───────────────────────────┘      └──────────────────────────────┘   └┘
974  
975  lemma mk_preimage_of_injective (f : α → β) (s : set β) (h : injective f) :
id                                                 └─┘        └───────┘ 
src                                                  └─┘         └───────┘
typ                                                └─┘        └───────┘ 
976    mk (f ⁻¹' s) ≤ mk s :=
id     └┘   └─┘    └┘ 
src    └┘    └─┘     └┘
typ    └┘   └─┘    └┘ 
doc    └┘    └─┘      └┘
977  by { convert mk_preimage_of_injective_lift.{u u} f s h using 1; rw [lift_id] }
id                └───────────────────────────┘                       └─────┘
src       └──────┘└───────────────────────────┘└─────┘   └──────┘  └──┘└─────┘└┘
typ       └──────┘└───────────────────────────┘└─────┘└──────┘  └──┘└─────┘└┘
doc       └──────┘                             └─────┘   └──────┘  └──┘       └┘
txt       └──────┘                             └─────┘   └──────┘  └──┘       └┘
par       └──────┘                             └─────┘   └──────┘  └──┘       └┘
pid                                           └─────┘   └─────┘    └┘       
st     └────────────────────────────────────────────────────────────────┘└─────┘└┘
978  
979  lemma mk_preimage_of_subset_range (f : α → β) (s : set β)
id                                                    └─┘ 
src                                                     └─┘
typ                                                   └─┘ 
980    (h : s ⊆ range f) : mk s ≤ mk (f ⁻¹' s) :=
id            └───┘     └┘   └┘   └─┘ 
src            └───┘      └┘    └┘    └─┘
typ           └───┘     └┘   └┘   └─┘ 
doc             └───┘      └┘     └┘    └─┘
981  by { convert mk_preimage_of_subset_range_lift.{u u} f s h using 1; rw [lift_id] }
id                └──────────────────────────────┘                       └─────┘
src       └──────┘└──────────────────────────────┘└─────┘   └──────┘  └──┘└─────┘└┘
typ       └──────┘└──────────────────────────────┘└─────┘└──────┘  └──┘└─────┘└┘
doc       └──────┘                                └─────┘   └──────┘  └──┘       └┘
txt       └──────┘                                └─────┘   └──────┘  └──┘       └┘
par       └──────┘                                └─────┘   └──────┘  └──┘       └┘
pid                                              └─────┘   └─────┘    └┘       
st     └───────────────────────────────────────────────────────────────────┘└─────┘└┘
982  
983  lemma mk_preimage_of_injective_of_subset_range (f : α → β) (s : set β)
id                                                                 └─┘ 
src                                                                  └─┘
typ                                                                └─┘ 
984    (h : injective f) (h2 : s ⊆ range f) : mk (f ⁻¹' s) = mk s :=
id          └───────┘           └───┘     └┘   └─┘    └┘ 
src         └───────┘             └───┘      └┘    └─┘     └┘
typ         └───────┘           └───┘     └┘   └─┘    └┘ 
doc                                └───┘      └┘    └─┘      └┘
985  by { convert mk_preimage_of_injective_of_subset_range_lift.{u u} f s h h2 using 1; rw [lift_id] }
id                └───────────────────────────────────────────┘          └┘              └─────┘
src       └──────┘└───────────────────────────────────────────┘└─────┘     └──────┘  └──┘└─────┘└┘
typ       └──────┘└───────────────────────────────────────────┘└─────┘└┘└──────┘  └──┘└─────┘└┘
doc       └──────┘                                             └─────┘     └──────┘  └──┘       └┘
txt       └──────┘                                             └─────┘     └──────┘  └──┘       └┘
par       └──────┘                                             └─────┘     └──────┘  └──┘       └┘
pid                                                           └─────┘     └─────┘    └┘       
st     └───────────────────────────────────────────────────────────────────────────────────┘└─────┘└┘
986  
987  lemma mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : set α}
id                                                                                    └─┘ 
src                                                                                     └─┘
typ                                                                                   └─┘ 
988    {t : set β} (h : t ⊆ f '' s) :
id          └─┘           └┘ 
src         └─┘              └┘
typ         └─┘           └┘ 
989      lift.{v u} (mk t) ≤ lift.{u v} (mk ({ x ∈ s | f x ∈ t } : set α)) :=
id       └──┘        └┘    └──┘        └┘                  └─┘ 
src      └──┘        └┘     └──┘        └┘                      └─┘
typ      └──┘        └┘    └──┘        └┘                  └─┘ 
doc      └──┘        └┘      └──┘        └┘
990  by { rw [image_eq_range] at h, convert mk_preimage_of_subset_range_lift _ _ h using 1, rw [mk_sep], refl }
id            └────────────┘                └──────────────────────────────┘                   └────┘
src       └──┘└────────────┘└────┘  └──────┘└──────────────────────────────┘└───┘ └──────┘  └──┘└────┘  └───┘
typ       └──┘└────────────┘└────┘  └──────┘└──────────────────────────────┘└───┘└──────┘  └──┘└────┘  └───┘
doc       └──┘              └────┘  └──────┘                                └───┘ └──────┘  └──┘        └───┘
txt       └──┘              └────┘  └──────┘                                └───┘ └──────┘  └──┘        └───┘
par       └──┘              └────┘  └──────┘                                └───┘ └──────┘  └──┘        └───┘
pid         └┘              └───┘                                         └───┘ └─────┘    └┘            
st     └───────────────────┘└───┘└──────────────────────────────────────────────────────┘└──────────┘└──────┘└┘
991  
992  lemma mk_subset_ge_of_subset_image (f : α → β) {s : set α} {t : set β} (h : t ⊆ f '' s) :
id                                                     └─┘        └─┘           └┘ 
src                                                      └─┘         └─┘              └┘
typ                                                    └─┘        └─┘           └┘ 
993    mk t ≤ mk ({ x ∈ s | f x ∈ t } : set α) :=
id     └┘   └┘                  └─┘ 
src    └┘    └┘                      └─┘
typ    └┘   └┘                  └─┘ 
doc    └┘     └┘
994  by { rw [image_eq_range] at h, convert mk_preimage_of_subset_range _ _ h using 1, rw [mk_sep], refl }
id            └────────────┘                └─────────────────────────┘                   └────┘
src       └──┘└────────────┘└────┘  └──────┘└─────────────────────────┘└───┘ └──────┘  └──┘└────┘  └───┘
typ       └──┘└────────────┘└────┘  └──────┘└─────────────────────────┘└───┘└──────┘  └──┘└────┘  └───┘
doc       └──┘              └────┘  └──────┘                           └───┘ └──────┘  └──┘        └───┘
txt       └──┘              └────┘  └──────┘                           └───┘ └──────┘  └──┘        └───┘
par       └──┘              └────┘  └──────┘                           └───┘ └──────┘  └──┘        └───┘
pid         └┘              └───┘                                    └───┘ └─────┘    └┘            
st     └───────────────────┘└───┘└─────────────────────────────────────────────────┘└──────────┘└──────┘└┘
995  
996  theorem le_mk_iff_exists_subset {c : cardinal} {α : Type u} {s : set α} :
id                                        └──────┘                    └─┘ 
src                                       └──────┘                    └─┘
typ                                       └──────┘                    └─┘ 
doc                                       └──────┘
997    c ≤ mk s ↔ ∃ p : set α, p ⊆ s ∧ mk p = c :=
id       └┘        └─┘      └┘   
src       └┘         └─┘         └┘   
typ      └┘        └─┘      └┘   
doc        └┘                          └┘
998  begin
st   └─────
999    rw [le_mk_iff_exists_set, ←subtype.exists_set_subtype],
id         └──────────────────┘   └────────────────────────┘
src    └──┘└──────────────────┘└─┘└────────────────────────┘
typ    └──┘└──────────────────┘└─┘└────────────────────────┘
doc    └──┘                    └─┘                          
txt    └──┘                    └─┘                          
par    └──┘                    └─┘                          
pid      └┘                    └─┘                          
st   ─────────────────────────┘└───────────────────────────┘└──
1000    apply exists_congr, intro t, rw [mk_image_eq], apply subtype.val_injective
id           └──────────┘               └─────────┘         └───────────────────┘
src    └────┘└──────────┘  └─────┘  └──┘└─────────┘  └────┘└───────────────────┘
typ    └────┘└──────────┘  └─────┘  └──┘└─────────┘  └────┘└───────────────────┘
doc    └────┘              └─────┘  └──┘             └────┘                     
txt    └────┘              └─────┘  └──┘             └────┘                     
par    └────┘              └─────┘  └──┘             └────┘                     
pid                            └┘    └┘                                       
st   ───────────────────┘└───────┘└───────────────┘└─────────────────────────────┘
1001  end
st   └─┘
1002  
1003  /-- The function α^{<β}, defined to be sup_{γ < β} α^γ.
1004    We index over {s : set β.out // mk s < β } instead of {γ // γ < β}, because the latter lives in a
1005    higher universe -/
1006  noncomputable def powerlt (α β : cardinal.{u}) : cardinal.{u} :=
id                                    └──────┘        └──────┘
src                                   └──────┘        └──────┘
typ                                   └──────┘        └──────┘
doc                                   └──────┘        └──────┘
1007  sup.{u u} (λ(s : {s : set β.out // mk s < β}), α ^ mk.{u} s)
id   └─┘                  └─┘ └──┘    └┘         └┘     
src  └─┘                  └─┘  └──┘    └┘            └┘
typ  └─┘                  └─┘ └──┘    └┘         └┘     
doc  └─┘                        └──┘    └┘             └┘
1008  
1009  infix ` ^< `:80 := powerlt
id                      └─────┘
src                     └─────┘
typ                     └─────┘
doc                     └─────┘
1010  
1011  theorem powerlt_aux {c c' : cardinal} (h : c < c') :
id                               └──────┘         └┘
src                              └──────┘         
typ                              └──────┘         └┘
doc                              └──────┘
1012    ∃(s : {s : set c'.out // mk s < c'}), mk s = c :=
id              └─┘ └┘└──┘    └┘   └┘   └┘   
src             └─┘   └──┘    └┘         └┘   
typ             └─┘ └┘└──┘    └┘   └┘   └┘   
doc                     └──┘    └┘           └┘
1013  begin
st   └─────
1014    cases out_embedding.mp (le_of_lt h) with f,
id           └──────────────┘  └──────┘ 
src    └────┘└──────────────┘ └──────┘ └──────┘
typ    └────┘└──────────────┘ └──────┘└──────┘
doc    └────┘                          └──────┘
txt    └────┘                          └──────┘
par    └────┘                          └──────┘
pid                                   └─────┘
st   ───────────────────────────────────────────┘└─
1015    have : mk ↥(range ⇑f) = c, { rwa [mk_range_eq, mk, quotient.out_eq c], exact f.2 },
id            └┘  └───┘             └─────────┘  └┘  └─────────────┘          
src    └─────┘└┘ └───┘ └┘     └───┘└─────────┘└┘└┘└┘└─────────────┘   └────┘ └─┘
typ    └─────┘└┘ └───┘└┘    └───┘└─────────┘└┘└┘└┘└─────────────┘  └────┘└─┘
doc    └─────┘└┘  └───┘  └┘      └───┘           └┘└┘└┘                  └────┘ └─┘
txt    └─────┘           └┘      └───┘           └┘  └┘                  └────┘ └─┘
par    └─────┘           └┘      └───┘           └┘  └┘                  └────┘ └─┘
pid    └───┘└┘           └┘         └┘           └┘  └┘                        └─┘
st   ──────────────────────────┘└──┘└──────────────┘└──┘└─────────────────┘└───────────┘└┘
1016    exact ⟨⟨range f, by convert h⟩, this⟩
id             └───┘                 └──┘
src    └────┘  └───┘ └┘  └──────┘ └─┘    └┘
typ    └────┘  └───┘└┘  └──────┘└─┘└──┘└┘
doc    └────┘  └───┘ └┘  └──────┘ └─┘    └┘
txt    └────┘        └┘  └──────┘ └─┘    └┘
par    └────┘        └┘  └──────┘ └─┘    └┘
pid                 └┘  └───────┘ └─┘    
st   ────────────────────┘└────────┘└───────┘
1017  end
st   └─┘
1018  
1019  lemma le_powerlt {c₁ c₂ c₃ : cardinal} (h : c₂ < c₃) : c₁ ^ c₂ ≤ c₁ ^< c₃ :=
id                                └──────┘       └┘  └┘    └┘  └┘  └┘ └┘ └┘
src                               └──────┘                            └┘
typ                               └──────┘       └┘  └┘    └┘  └┘  └┘ └┘ └┘
doc                               └──────┘                              └┘
1020  by { rcases powerlt_aux h with ⟨s, rfl⟩, apply le_sup _ s }
id               └─────────┘                       └────┘   
src       └─────┘└─────────┘ └────────────┘  └────┘└────┘└─┘ 
typ       └─────┘└─────────┘└────────────┘  └────┘└────┘└─┘
doc       └─────┘            └────────────┘  └────┘      └─┘ 
txt       └─────┘            └────────────┘  └────┘      └─┘ 
par       └─────┘            └────────────┘  └────┘      └─┘ 
pid                         └────────────┘             └─┘ 
st     └───────────────────────────────────┘└─────────────────┘└┘
1021  
1022  lemma powerlt_le {c₁ c₂ c₃ : cardinal} : c₁ ^< c₂ ≤ c₃ ↔ ∀(c₄ < c₂), c₁ ^ c₄ ≤ c₃ :=
id                                └──────┘    └┘ └┘ └┘  └┘   └┘   └┘   └┘  └┘  └┘
src                               └──────┘       └┘                            
typ                               └──────┘    └┘ └┘ └┘  └┘   └┘   └┘   └┘  └┘  └┘
doc                               └──────┘       └┘                          
1023  begin
st   └─────
1024    rw [powerlt, sup_le],
id         └─────┘  └────┘
src    └──┘└─────┘└┘└────┘
typ    └──┘└─────┘└┘└────┘
doc    └──┘└─────┘└┘      
txt    └──┘       └┘      
par    └──┘       └┘      
pid      └┘       └┘      
st   ────────────┘└──────┘└──
1025    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
1026    { intros h c₄ hc₄, rcases powerlt_aux hc₄ with ⟨s, rfl⟩, exact h s },
id                               └─────────┘ └─┘                       
src      └─────────────┘  └─────┘└─────────┘   └────────────┘  └────┘  
typ      └─────────────┘  └─────┘└─────────┘└─┘└────────────┘  └────┘
doc      └─────────────┘  └─────┘              └────────────┘  └────┘  
txt      └─────────────┘  └─────┘              └────────────┘  └────┘  
par      └─────────────┘  └─────┘              └────────────┘  └────┘  
pid            └───────┘                      └────────────┘         
st   ───┘└─────────────┘└────────────────────────────────────┘└──────────┘└┘
1027    intros h s, exact h _ s.2
id                          
src    └────────┘  └────┘ └─┘ └─┘
typ    └────────┘  └────┘└─┘└─┘
doc    └────────┘  └────┘ └─┘ └─┘
txt    └────────┘  └────┘ └─┘ └─┘
par    └────────┘  └────┘ └─┘ └─┘
pid          └──┘        └─┘ └─┘
st   ───────────┘└──────────────┘
1028  end
st   └─┘
1029  
1030  lemma powerlt_le_powerlt_left {a b c : cardinal} (h : b ≤ c) : a ^< b ≤ a ^< c :=
id                                          └──────┘              └┘    └┘ 
src                                         └──────┘                 └┘      └┘
typ                                         └──────┘              └┘    └┘ 
doc                                         └──────┘                  └┘       └┘
1031  by { rw [powerlt, sup_le], rintro ⟨s, hs⟩, apply le_powerlt, exact lt_of_lt_of_le hs h }
id            └─────┘  └────┘                         └────────┘        └────────────┘ └┘ 
src       └──┘└─────┘└┘└────┘  └────────────┘  └────┘└────────┘  └────┘└────────────┘   
typ       └──┘└─────┘└┘└────┘  └────────────┘  └────┘└────────┘  └────┘└────────────┘└┘
doc       └──┘└─────┘└┘        └────────────┘  └────┘            └────┘                 
txt       └──┘       └┘        └────────────┘  └────┘            └────┘                 
par       └──┘       └┘        └────────────┘  └────┘            └────┘                 
pid         └┘       └┘              └──────┘                                         
st     └────────────┘└──────┘└───────────────┘└────────────────┘└──────────────────────────┘└┘
1032  
1033  lemma powerlt_succ {c₁ c₂ : cardinal} (h : c₁ ≠ 0) : c₁ ^< c₂.succ = c₁ ^ c₂ :=
id                               └──────┘       └┘       └┘ └┘ └┘└───┘  └┘  └┘
src                              └──────┘                   └┘   └───┘     
typ                              └──────┘       └┘       └┘ └┘ └┘└───┘  └┘  └┘
doc                              └──────┘                    └┘   └───┘      
1034  begin
st   └─────
1035    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
1036    { rw powerlt_le, intros c₃ h2, apply power_le_power_left h, rwa [←lt_succ] },
id          └────────┘                      └─────────────────┘         └─────┘
src      └─┘└────────┘  └──────────┘  └────┘└─────────────────┘   └────┘└─────┘└┘
typ      └─┘└────────┘  └──────────┘  └────┘└─────────────────┘  └────┘└─────┘└┘
doc      └─┘            └──────────┘  └────┘                      └────┘       └┘
txt      └─┘            └──────────┘  └────┘                      └────┘       └┘
par      └─┘            └──────────┘  └────┘                      └────┘       └┘
pid                          └────┘                                └─┘       
st   ───┘└───────────┘└────────────┘└───────────────────────────┘└─────────────┘└┘
1037    { apply le_powerlt, apply lt_succ_self }
id             └────────┘        └──────────┘
src      └────┘└────────┘  └────┘└──────────┘
typ      └────┘└────────┘  └────┘└──────────┘
doc      └────┘            └────┘            
txt      └────┘            └────┘            
par      └────┘            └────┘            
pid                                        
st   ───────────────────┘└───────────────────┘└─
1038  end
st   ──┘
1039  
1040  lemma powerlt_max {c₁ c₂ c₃ : cardinal} : c₁ ^< max c₂ c₃ = max (c₁ ^< c₂) (c₁ ^< c₃) :=
id                                 └──────┘    └┘ └┘ └─┘ └┘ └┘  └─┘  └┘ └┘ └┘   └┘ └┘ └┘
src                                └──────┘       └┘ └─┘        └─┘     └┘         └┘
typ                                └──────┘    └┘ └┘ └─┘ └┘ └┘  └─┘  └┘ └┘ └┘   └┘ └┘ └┘
doc                                └──────┘       └┘                     └┘         └┘
1041  by { cases le_total c₂ c₃; simp only [max_eq_left, max_eq_right, h, powerlt_le_powerlt_left] }
id              └──────┘ └┘ └┘             └─────────┘  └──────────┘    └─────────────────────┘
src       └────┘└──────┘      └─────────┘└─────────┘└┘└──────────┘└┘ └┘└─────────────────────┘└┘
typ       └────┘└──────┘└┘└┘  └─────────┘└─────────┘└┘└──────────┘└┘└┘└─────────────────────┘└┘
doc       └────┘              └─────────┘           └┘            └┘ └┘                       └┘
txt       └────┘              └─────────┘           └┘            └┘ └┘                       └┘
par       └────┘              └─────────┘           └┘            └┘ └┘                       └┘
pid                              └──┘└┘           └┘            └┘ └┘                       
st     └─────────────────────────────────────────────────────────────────────────────────────────┘└┘
1042  
1043  lemma zero_powerlt {a : cardinal} (h : a ≠ 0) : 0 ^< a = 1 :=
id                           └──────┘                └┘  
src                          └──────┘                 └┘   
typ                          └──────┘                └┘  
doc                          └──────┘                  └┘
1044  begin
st   └─────
1045    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
1046    { rw [powerlt_le], intros c hc, apply zero_power_le },
id           └────────┘                      └───────────┘
src      └──┘└────────┘  └─────────┘  └────┘└───────────┘
typ      └──┘└────────┘  └─────────┘  └────┘└───────────┘
doc      └──┘            └─────────┘  └────┘             
txt      └──┘            └─────────┘  └────┘             
par      └──┘            └─────────┘  └────┘             
pid        └┘                  └───┘                    
st   ───┘└────────────┘└────────────┘└────────────────────┘└┘
1047    convert le_powerlt (pos_iff_ne_zero.2 h), rw [power_zero]
id             └────────┘  └─────────────┘          └────────┘
src    └──────┘└────────┘ └─────────────┘└─┘   └──┘└────────┘└┘
typ    └──────┘└────────┘ └─────────────┘└─┘  └──┘└────────┘└┘
doc    └──────┘                          └─┘   └──┘          └┘
txt    └──────┘                          └─┘   └──┘          └┘
par    └──────┘                          └─┘   └──┘          └┘
pid                                     └─┘     └┘          
st   ─────────────────────────────────────────┘└──────────────┘
1048  end
st   └─┘
1049  
1050  lemma powerlt_zero {a : cardinal} : a ^< 0 = 0 :=
id                           └──────┘     └┘   
src                          └──────┘      └┘   
typ                          └──────┘     └┘   
doc                          └──────┘      └┘
1051  by { apply sup_eq_zero, rintro ⟨x, hx⟩, rw [←not_le] at hx, apply hx, apply zero_le }
id              └─────────┘                       └────┘                         └─────┘
src       └────┘└─────────┘  └────────────┘  └───┘└────┘└─────┘  └────┘    └────┘└─────┘
typ       └────┘└─────────┘  └────────────┘  └───┘└────┘└─────┘  └────┘    └────┘└─────┘
doc       └────┘             └────────────┘  └───┘      └─────┘  └────┘    └────┘       
txt       └────┘             └────────────┘  └───┘      └─────┘  └────┘    └────┘       
par       └────┘             └────────────┘  └───┘      └─────┘  └────┘    └────┘       
pid                               └──────┘    └─┘      └────┘                       
st     └──────────────────┘└──────────────┘└───────────┘└────┘└────────┘└──────────────┘└┘
1052  
1053  end cardinal